Step | Hyp | Ref
| Expression |
1 | | stoweidlem27.4 |
. . . 4
   |
2 | | stoweidlem27.5 |
. . . 4
   |
3 | | fnex 5920 |
. . . 4
     |
4 | 1, 2, 3 | syl2anc 643 |
. . 3
   |
5 | | stoweidlem27.7 |
. . . . 5
           |
6 | | f1ofn 5634 |
. . . . 5
               |
7 | 5, 6 | syl 16 |
. . . 4
       |
8 | | ovex 6065 |
. . . 4
     |
9 | | fnex 5920 |
. . . 4
             |
10 | 7, 8, 9 | sylancl 644 |
. . 3
   |
11 | | coexg 5371 |
. . 3
 
     |
12 | 4, 10, 11 | syl2anc 643 |
. 2
     |
13 | | stoweidlem27.3 |
. . 3
   |
14 | | f1of 5633 |
. . . . . . 7
                   |
15 | 5, 14 | syl 16 |
. . . . . 6
           |
16 | | fnfco 5568 |
. . . . . 6
           
       |
17 | 1, 15, 16 | syl2anc 643 |
. . . . 5
         |
18 | | rncoss 5095 |
. . . . . 6

  |
19 | | fvelrnb 5733 |
. . . . . . . . . . . 12
  
        |
20 | 1, 19 | syl 16 |
. . . . . . . . . . 11
  
        |
21 | 20 | biimpa 471 |
. . . . . . . . . 10
 
         |
22 | | simpr 448 |
. . . . . . . . . . . . . . 15
 
   |
23 | | stoweidlem27.1 |
. . . . . . . . . . . . . . . . 17
 

        |
24 | 23 | elrnmpt 5076 |
. . . . . . . . . . . . . . . 16
  

          |
25 | 22, 24 | syl 16 |
. . . . . . . . . . . . . . 15
 
              |
26 | 22, 25 | mpbid 202 |
. . . . . . . . . . . . . 14
 
 


        |
27 | | stoweidlem27.10 |
. . . . . . . . . . . . . . . 16
   |
28 | | nfmpt1 4258 |
. . . . . . . . . . . . . . . . . . 19
   

        |
29 | 23, 28 | nfcxfr 2537 |
. . . . . . . . . . . . . . . . . 18
   |
30 | 29 | nfrn 5071 |
. . . . . . . . . . . . . . . . 17
   |
31 | 30 | nfcri 2534 |
. . . . . . . . . . . . . . . 16

 |
32 | 27, 31 | nfan 1842 |
. . . . . . . . . . . . . . 15
  
  |
33 | | nfv 1626 |
. . . . . . . . . . . . . . 15
       |
34 | | stoweidlem27.6 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
35 | 34 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . 19
   
 


      
      |
36 | | simpr 448 |
. . . . . . . . . . . . . . . . . . 19
   
 


      


        |
37 | 35, 36 | eleqtrd 2480 |
. . . . . . . . . . . . . . . . . 18
   
 


      
    

        |
38 | | nfcv 2540 |
. . . . . . . . . . . . . . . . . . 19
       |
39 | | stoweidlem27.11 |
. . . . . . . . . . . . . . . . . . 19
   |
40 | | nfv 1626 |
. . . . . . . . . . . . . . . . . . 19


          |
41 | | fveq1 5686 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
42 | 41 | breq2d 4184 |
. . . . . . . . . . . . . . . . . . . . 21
     
   
           |
43 | 42 | rabbidv 2908 |
. . . . . . . . . . . . . . . . . . . 20
                       |
44 | 43 | eqeq2d 2415 |
. . . . . . . . . . . . . . . . . . 19
           
             |
45 | 38, 39, 40, 44 | elrabf 3051 |
. . . . . . . . . . . . . . . . . 18
            
                  |
46 | 37, 45 | sylib 189 |
. . . . . . . . . . . . . . . . 17
   
 


      
    
             |
47 | 46 | simpld 446 |
. . . . . . . . . . . . . . . 16
   
 


      
      |
48 | 47 | exp31 588 |
. . . . . . . . . . . . . . 15
 
   

              |
49 | 32, 33, 48 | rexlimd 2787 |
. . . . . . . . . . . . . 14
 
  

      
       |
50 | 26, 49 | mpd 15 |
. . . . . . . . . . . . 13
 
       |
51 | 50 | adantlr 696 |
. . . . . . . . . . . 12
   
       |
52 | | eleq1 2464 |
. . . . . . . . . . . 12
         
   |
53 | 51, 52 | syl5ibcom 212 |
. . . . . . . . . . 11
   
     
   |
54 | 53 | reximdva 2778 |
. . . . . . . . . 10
 
  
     
   |
55 | 21, 54 | mpd 15 |
. . . . . . . . 9
 
    |
56 | | idd 22 |
. . . . . . . . . . 11
     |
57 | 56 | a1i 11 |
. . . . . . . . . 10
 
       |
58 | 57 | rexlimdv 2789 |
. . . . . . . . 9
 
  
   |
59 | 55, 58 | mpd 15 |
. . . . . . . 8
 
   |
60 | 59 | ex 424 |
. . . . . . 7
     |
61 | 60 | ssrdv 3314 |
. . . . . 6
   |
62 | 18, 61 | syl5ss 3319 |
. . . . 5
     |
63 | | df-f 5417 |
. . . . 5
          
 
    
     |
64 | 17, 62, 63 | sylanbrc 646 |
. . . 4
             |
65 | | stoweidlem27.9 |
. . . . 5
   |
66 | | stoweidlem27.8 |
. . . . . . . . . 10
  
   |
67 | 66 | sselda 3308 |
. . . . . . . . 9
 

 
   |
68 | | eluni 3978 |
. . . . . . . . 9
 
  
   |
69 | 67, 68 | sylib 189 |
. . . . . . . 8
 

 
  
   |
70 | | nfv 1626 |
. . . . . . . . . 10

   |
71 | 27, 70 | nfan 1842 |
. . . . . . . . 9
  
    |
72 | 23 | funmpt2 5449 |
. . . . . . . . . . . . . . 15
 |
73 | 23 | dmeqi 5030 |
. . . . . . . . . . . . . . . . . 18
           |
74 | | stoweidlem27.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
75 | 39 | rabexgf 27562 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
      
  |
76 | 74, 75 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
 

        |
77 | 76 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
      
  |
78 | 77 | ex 424 |
. . . . . . . . . . . . . . . . . . . 20
  

         |
79 | 27, 78 | ralrimi 2747 |
. . . . . . . . . . . . . . . . . . 19
  

        |
80 | | dmmptg 5326 |
. . . . . . . . . . . . . . . . . . 19
 


     


          |
81 | 79, 80 | syl 16 |
. . . . . . . . . . . . . . . . . 18
             |
82 | 73, 81 | syl5eq 2448 |
. . . . . . . . . . . . . . . . 17
   |
83 | 82 | eleq2d 2471 |
. . . . . . . . . . . . . . . 16
     |
84 | 83 | biimpar 472 |
. . . . . . . . . . . . . . 15
 
   |
85 | | fvelrn 5825 |
. . . . . . . . . . . . . . 15
         |
86 | 72, 84, 85 | sylancr 645 |
. . . . . . . . . . . . . 14
 
       |
87 | 86 | adantrl 697 |
. . . . . . . . . . . . 13
 

        |
88 | | f1ofo 5640 |
. . . . . . . . . . . . . . . . . . . 20
                   |
89 | | forn 5615 |
. . . . . . . . . . . . . . . . . . . 20
           |
90 | 5, 88, 89 | 3syl 19 |
. . . . . . . . . . . . . . . . . . 19
   |
91 | 90 | eleq2d 2471 |
. . . . . . . . . . . . . . . . . 18
             |
92 | 91 | biimpar 472 |
. . . . . . . . . . . . . . . . 17
 
    
      |
93 | 7 | adantr 452 |
. . . . . . . . . . . . . . . . . 18
 
    
      |
94 | | fvelrnb 5733 |
. . . . . . . . . . . . . . . . . 18
                           |
95 | 93, 94 | syl 16 |
. . . . . . . . . . . . . . . . 17
 
    
    
                 |
96 | 92, 95 | mpbid 202 |
. . . . . . . . . . . . . . . 16
 
    
                |
97 | | df-rex 2672 |
. . . . . . . . . . . . . . . 16
              
                  |
98 | 96, 97 | sylib 189 |
. . . . . . . . . . . . . . 15
 
    
                  |
99 | | simprl 733 |
. . . . . . . . . . . . . . . . . 18
                             |
100 | 15 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
101 | | fvco3 5759 |
. . . . . . . . . . . . . . . . . . . . 21
         
                     |
102 | 100, 99, 101 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
103 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
104 | 103 | ad2antll 710 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
105 | 102, 104 | eqtrd 2436 |
. . . . . . . . . . . . . . . . . . 19
                                       |
106 | | eleq1 2464 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
107 | 106 | anbi2d 685 |
. . . . . . . . . . . . . . . . . . . . . . 23
      

         |
108 | | eleq2 2465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
           |
109 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
110 | 109 | eleq1d 2470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
               |
111 | 108, 110 | bitrd 245 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
               |
112 | 107, 111 | imbi12d 312 |
. . . . . . . . . . . . . . . . . . . . . 22
       
            
                |
113 | 112, 34 | vtoclg 2971 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
114 | 113 | anabsi7 793 |
. . . . . . . . . . . . . . . . . . . 20
 
    
              |
115 | 114 | adantr 452 |
. . . . . . . . . . . . . . . . . . 19
                                     |
116 | 105, 115 | eqeltrd 2478 |
. . . . . . . . . . . . . . . . . 18
                                   |
117 | 99, 116 | jca 519 |
. . . . . . . . . . . . . . . . 17
                                         |
118 | 117 | ex 424 |
. . . . . . . . . . . . . . . 16
 
    
                                  |
119 | 118 | eximdv 1629 |
. . . . . . . . . . . . . . 15
 
    
       
        
                     |
120 | 98, 119 | mpd 15 |
. . . . . . . . . . . . . 14
 
    
                    |
121 | | df-rex 2672 |
. . . . . . . . . . . . . 14
                                     |
122 | 120, 121 | sylibr 204 |
. . . . . . . . . . . . 13
 
    
                  |
123 | 87, 122 | syldan 457 |
. . . . . . . . . . . 12
 

  
                 |
124 | | simplrl 737 |
. . . . . . . . . . . . . . . . 17
   
 
 
        
  |
125 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
126 | 23 | fvmpt2 5771 |
. . . . . . . . . . . . . . . . . . . . . . 23
  

      
    

        |
127 | 125, 77, 126 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     

        |
128 | 127 | eleq2d 2471 |
. . . . . . . . . . . . . . . . . . . . 21
 
           
 
    

         |
129 | 128 | biimpa 471 |
. . . . . . . . . . . . . . . . . . . 20
                     

        |
130 | 129 | adantlrl 701 |
. . . . . . . . . . . . . . . . . . 19
   
 
 
        
 
    

        |
131 | | nfcv 2540 |
. . . . . . . . . . . . . . . . . . . 20
         |
132 | | nfv 1626 |
. . . . . . . . . . . . . . . . . . . 20


            |
133 | | fveq1 5686 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
134 | 133 | breq2d 4184 |
. . . . . . . . . . . . . . . . . . . . . 22
       
   
             |
135 | 134 | rabbidv 2908 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
136 | 135 | eqeq2d 2415 |
. . . . . . . . . . . . . . . . . . . 20
             
               |
137 | 131, 39, 132, 136 | elrabf 3051 |
. . . . . . . . . . . . . . . . . . 19
       

            

              |
138 | 130, 137 | sylib 189 |
. . . . . . . . . . . . . . . . . 18
   
 
 
        
      
               |
139 | 138 | simprd 450 |
. . . . . . . . . . . . . . . . 17
   
 
 
        
              |
140 | 124, 139 | eleqtrd 2480 |
. . . . . . . . . . . . . . . 16
   
 
 
        

             |
141 | | rabid 2844 |
. . . . . . . . . . . . . . . 16
            

             |
142 | 140, 141 | sylib 189 |
. . . . . . . . . . . . . . 15
   
 
 
        

             |
143 | 142 | simprd 450 |
. . . . . . . . . . . . . 14
   
 
 
        
            |
144 | 143 | ex 424 |
. . . . . . . . . . . . 13
 

                          |
145 | 144 | reximdv 2777 |
. . . . . . . . . . . 12
 

                                      |
146 | 123, 145 | mpd 15 |
. . . . . . . . . . 11
 

  
                 |
147 | 146 | ex 424 |
. . . . . . . . . 10
                       |
148 | 147 | adantr 452 |
. . . . . . . . 9
 

 
 
                    |
149 | 71, 148 | eximd 1782 |
. . . . . . . 8
 

 
       
                  |
150 | 69, 149 | mpd 15 |
. . . . . . 7
 

 
  
                 |
151 | | nfv 1626 |
. . . . . . . 8
  
                |
152 | | idd 22 |
. . . . . . . 8
 

 
 
                                  |
153 | 71, 151, 152 | exlimd 1820 |
. . . . . . 7
 

 
                                      |
154 | 150, 153 | mpd 15 |
. . . . . 6
 

 
                  |
155 | 154 | ex 424 |
. . . . 5
                       |
156 | 65, 155 | ralrimi 2747 |
. . . 4
                       |
157 | 64, 156 | jca 519 |
. . 3
                                   |
158 | 13, 157 | jca 519 |
. 2
                                     |
159 | | feq1 5535 |
. . . . 5
                         |
160 | | fveq1 5686 |
. . . . . . . . 9
               |
161 | 160 | fveq1d 5689 |
. . . . . . . 8
                       |
162 | 161 | breq2d 4184 |
. . . . . . 7
   
       
             |
163 | 162 | rexbidv 2687 |
. . . . . 6
    
            
                   |
164 | 163 | ralbidv 2686 |
. . . . 5
    
                
                       |
165 | 159, 164 | anbi12d 692 |
. . . 4
                                           
                       |
166 | 165 | anbi2d 685 |
. . 3
                                 
                                     |
167 | 166 | spcegv 2997 |
. 2
                                                                         |
168 | 12, 158, 167 | sylc 58 |
1
                                   |