Step | Hyp | Ref
| Expression |
1 | | stoweidlem31.14 |
. . 3
   |
2 | | fnchoice 37413 |
. . 3
   
  
        |
3 | 1, 2 | syl 17 |
. 2
               |
4 | | vex 3034 |
. . . . 5
 |
5 | | stoweidlem31.6 |
. . . . . . 7
   
          
     
                |
6 | | stoweidlem31.12 |
. . . . . . . . 9
   |
7 | | stoweidlem31.7 |
. . . . . . . . 9

  |
8 | 6, 7 | ssexd 4543 |
. . . . . . . 8
   |
9 | | mptexg 6151 |
. . . . . . . 8
         
    

                       |
10 | 8, 9 | syl 17 |
. . . . . . 7
    
          
     
                 |
11 | 5, 10 | syl5eqel 2553 |
. . . . . 6
   |
12 | | vex 3034 |
. . . . . 6
 |
13 | | coexg 6763 |
. . . . . 6
 
     |
14 | 11, 12, 13 | sylancl 675 |
. . . . 5
     |
15 | | coexg 6763 |
. . . . 5
  
   
    |
16 | 4, 14, 15 | sylancr 676 |
. . . 4
  
    |
17 | 16 | adantr 472 |
. . 3
 
 
               |
18 | | simprl 772 |
. . . . . 6
 
 
           |
19 | | stoweidlem31.1 |
. . . . . . . . 9
   |
20 | | nfcv 2612 |
. . . . . . . . . . 11
   |
21 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
22 | | nfrab1 2957 |
. . . . . . . . . . . . . 14
  
 
          
     
               |
23 | 21, 22 | nfmpt 4484 |
. . . . . . . . . . . . 13
     
          
     
                |
24 | 5, 23 | nfcxfr 2610 |
. . . . . . . . . . . 12
   |
25 | 24 | nfrn 5083 |
. . . . . . . . . . 11
   |
26 | 20, 25 | nffn 5682 |
. . . . . . . . . 10

 |
27 | | nfv 1769 |
. . . . . . . . . . 11
         |
28 | 25, 27 | nfral 2789 |
. . . . . . . . . 10
  
        |
29 | 26, 28 | nfan 2031 |
. . . . . . . . 9
     
       |
30 | 19, 29 | nfan 2031 |
. . . . . . . 8
  
            |
31 | | fvelrnb 5926 |
. . . . . . . . . . . . 13
           |
32 | 18, 31 | syl 17 |
. . . . . . . . . . . 12
 
 
         
         |
33 | 32 | biimpa 492 |
. . . . . . . . . . 11
                       |
34 | | nfv 1769 |
. . . . . . . . . . . . . 14
   |
35 | | nfv 1769 |
. . . . . . . . . . . . . . 15
  |
36 | | nfra1 2785 |
. . . . . . . . . . . . . . 15
           |
37 | 35, 36 | nfan 2031 |
. . . . . . . . . . . . . 14
     
       |
38 | 34, 37 | nfan 2031 |
. . . . . . . . . . . . 13
               |
39 | | nfv 1769 |
. . . . . . . . . . . . 13
  |
40 | 38, 39 | nfan 2031 |
. . . . . . . . . . . 12
       
      
  |
41 | | simp3 1032 |
. . . . . . . . . . . . . 14
       
      
     
      |
42 | | simp1ll 1093 |
. . . . . . . . . . . . . . 15
       
      
     
  |
43 | | simplrr 779 |
. . . . . . . . . . . . . . . 16
                 
       |
44 | 43 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . 15
       
      
     
  
       |
45 | | simp2 1031 |
. . . . . . . . . . . . . . 15
       
      
     
  |
46 | | simp3 1032 |
. . . . . . . . . . . . . . . . 17
 
  
        |
47 | | 3simpc 1029 |
. . . . . . . . . . . . . . . . . 18
 
  
         
        |
48 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
49 | | stoweidlem31.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
50 | | stoweidlem31.13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
51 | | rabexg 4549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 
        
                        |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
          
     
                |
53 | 52 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
          
     
                 |
54 | 49, 53 | ralrimi 2800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
 
          
     
                |
55 | 5 | fnmpt 5714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       
    

                      |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
57 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
58 | | fvelrnb 5926 |
. . . . . . . . . . . . . . . . . . . . . . 23
          |
59 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
          
     
                |
60 | 5, 59 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
61 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
62 | 60, 61 | nffv 5886 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
63 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
64 | 62, 63 | nfeq 2623 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
65 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
66 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
67 | 66 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
68 | 64, 65, 67 | cbvrex 3002 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

      |
69 | 58, 68 | syl6bb 269 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
70 | 57, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
          |
71 | 48, 70 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20
 
 
      |
72 | 60 | nfrn 5083 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
73 | 72 | nfcri 2606 |
. . . . . . . . . . . . . . . . . . . . . 22

 |
74 | 49, 73 | nfan 2031 |
. . . . . . . . . . . . . . . . . . . . 21
  
  |
75 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . 21
  |
76 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
      |
77 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
78 | 50 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
79 | 78, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 
 
        
                        |
80 | 5 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
    

                         
 
        
                        |
81 | 77, 79, 80 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       
          
     
                |
82 | 7 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
83 | | stoweidlem31.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             
           
       |
84 | 83 | rabeq2i 3028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30


   
          
                  |
85 | 82, 84 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   
 

         
                  |
86 | 85 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    
          
                 |
87 | | stoweidlem31.10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
88 | | stoweidlem31.8 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
89 | 88 | nnrpd 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
90 | 87, 89 | rpdivcld 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
91 | 90 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
     |
92 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       
         |
93 | 92 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
   

         |
94 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
95 | 94 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
   
           |
96 | 95 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
        
               |
97 | 93, 96 | 3anbi23d 1368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
    

         
    
 

         
     
                |
98 | 97 | rexbidv 2892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
          
           
    

 

         
     
                |
99 | 98 | rspccva 3135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
              
           
     
             
                       |
100 | 86, 91, 99 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 
 

         
     
               |
101 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

 |
102 | 19, 101 | nfan 2031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
  |
103 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
104 | 22, 103 | nfne 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
 
          
     
               |
105 | | 3simpc 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 
        
                        

         
     
                |
106 | | rabid 2953 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   

         
     
             

 
        
                        |
107 | 105, 106 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
        
                             
    

                      |
108 | | ne0i 3728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   

         
     
              
 
        
                        |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
        
                        

         
     
                |
110 | 109 | 3exp 1230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    
          
     
            

 
        
                          |
111 | 102, 104,
110 | rexlimd 2866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
          
                     
 
          
     
                 |
112 | 100, 111 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 
 
        
                        |
113 | 81, 112 | eqnetrd 2710 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
114 | 113 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
      |
115 | 76, 114 | eqnetrrd 2711 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
  |
116 | 115 | 3adant1r 1285 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       |
117 | 116 | 3exp 1230 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
118 | 74, 75, 117 | rexlimd 2866 |
. . . . . . . . . . . . . . . . . . . 20
 
  
       |
119 | 71, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
 
   |
120 | 119 | 3adant2 1049 |
. . . . . . . . . . . . . . . . . 18
 
  
        |
121 | | rspa 2774 |
. . . . . . . . . . . . . . . . . 18
                   |
122 | 47, 120, 121 | sylc 61 |
. . . . . . . . . . . . . . . . 17
 
  
            |
123 | 46, 122 | jca 541 |
. . . . . . . . . . . . . . . 16
 
  
              |
124 | | vex 3034 |
. . . . . . . . . . . . . . . . . 18
 |
125 | 5 | elrnmpt 5087 |
. . . . . . . . . . . . . . . . . 18
     

         
     
                 |
126 | 124, 125 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17



 
          
     
                |
127 | 46, 126 | sylib 201 |
. . . . . . . . . . . . . . . 16
 
  
      

 
        
                        |
128 | | nfv 1769 |
. . . . . . . . . . . . . . . . . 18
       |
129 | 73, 128 | nfan 2031 |
. . . . . . . . . . . . . . . . 17
         |
130 | | nfv 1769 |
. . . . . . . . . . . . . . . . 17
       |
131 | | simp1r 1055 |
. . . . . . . . . . . . . . . . . . 19
          
          
     
                     |
132 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . 19
          
          
     
               
 
        
                        |
133 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . 22
     

 
        
                      
      |
134 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . 22
     

 
        
                      

 
          
     
                |
135 | 133, 134 | eleqtrd 2551 |
. . . . . . . . . . . . . . . . . . . . 21
     

 
        
                      
           
    

                      |
136 | | elrabi 3181 |
. . . . . . . . . . . . . . . . . . . . . 22
       

         
     
                    |
137 | | fveq1 5878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
138 | 137 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
   
           |
139 | 137 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
           |
140 | 138, 139 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
              
                 
    |
141 | 140 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
        
 
                
    |
142 | 137 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
 
             |
143 | 142 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
   
 

             |
144 | 137 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             
               |
145 | 144 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
          
                   |
146 | 141, 143,
145 | 3anbi123d 1365 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
    

                  
 

                 
         
                    |
147 | 146 | elrab 3184 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       

         
     
             
    
 
                
                                |
148 | 147 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
       

         
     
               
                
                               |
149 | 148 | simp1d 1042 |
. . . . . . . . . . . . . . . . . . . . . 22
       

         
     
              
                    |
150 | 141 | elrab 3184 |
. . . . . . . . . . . . . . . . . . . . . 22
      
          
    

                     |
151 | 136, 149,
150 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . 21
       

         
     
                            
    |
152 | 135, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
     

 
        
                      
     
        
    |
153 | | stoweidlem31.4 |
. . . . . . . . . . . . . . . . . . . 20
          
   |
154 | 152, 153 | syl6eleqr 2560 |
. . . . . . . . . . . . . . . . . . 19
     

 
        
                      
      |
155 | 131, 132,
154 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
          
          
     
                     |
156 | 155 | 3exp 1230 |
. . . . . . . . . . . . . . . . 17
       
   
          
     
                      |
157 | 129, 130,
156 | rexlimd 2866 |
. . . . . . . . . . . . . . . 16
        

 
          
     
                     |
158 | 123, 127,
157 | sylc 61 |
. . . . . . . . . . . . . . 15
 
  
            |
159 | 42, 44, 45, 158 | syl3anc 1292 |
. . . . . . . . . . . . . 14
       
      
     
      |
160 | 41, 159 | eqeltrrd 2550 |
. . . . . . . . . . . . 13
       
      
     
  |
161 | 160 | 3exp 1230 |
. . . . . . . . . . . 12
                         |
162 | 40, 161 | reximdai 2853 |
. . . . . . . . . . 11
                
     
   |
163 | 33, 162 | mpd 15 |
. . . . . . . . . 10
                  |
164 | | nfv 1769 |
. . . . . . . . . . 11
  |
165 | | idd 24 |
. . . . . . . . . . . 12
     |
166 | 165 | a1i 11 |
. . . . . . . . . . 11
                     |
167 | 40, 164, 166 | rexlimd 2866 |
. . . . . . . . . 10
                
   |
168 | 163, 167 | mpd 15 |
. . . . . . . . 9
                 |
169 | 168 | ex 441 |
. . . . . . . 8
 
 
             |
170 | 30, 169 | ralrimi 2800 |
. . . . . . 7
 
 
         
  |
171 | | dfss3 3408 |
. . . . . . . 8

   |
172 | | nfrab1 2957 |
. . . . . . . . . . 11
  
         
   |
173 | 153, 172 | nfcxfr 2610 |
. . . . . . . . . 10
   |
174 | 173 | nfcri 2606 |
. . . . . . . . 9

 |
175 | | nfv 1769 |
. . . . . . . . 9
  |
176 | | eleq1 2537 |
. . . . . . . . 9
 
   |
177 | 174, 175,
176 | cbvral 3001 |
. . . . . . . 8
 
   |
178 | 171, 177 | bitri 257 |
. . . . . . 7

   |
179 | 170, 178 | sylibr 217 |
. . . . . 6
 
 
        
  |
180 | | df-f 5593 |
. . . . . 6
    
    |
181 | 18, 179, 180 | sylanbrc 677 |
. . . . 5
 
 
               |
182 | | dffn3 5748 |
. . . . . . . 8

      |
183 | 56, 182 | sylib 201 |
. . . . . . 7
       |
184 | 183 | adantr 472 |
. . . . . 6
 
 
               |
185 | | stoweidlem31.9 |
. . . . . . . 8
           |
186 | | f1of 5828 |
. . . . . . . 8
        
          |
187 | 185, 186 | syl 17 |
. . . . . . 7
           |
188 | 187 | adantr 472 |
. . . . . 6
 
 
                   |
189 | | fco 5751 |
. . . . . 6
              
            |
190 | 184, 188,
189 | syl2anc 673 |
. . . . 5
 
 
                     |
191 | | fco 5751 |
. . . . 5
                  
            |
192 | 181, 190,
191 | syl2anc 673 |
. . . 4
 
 
                       |
193 | | fvco3 5957 |
. . . . . . . . 9
           
       
                 |
194 | 190, 193 | sylan 479 |
. . . . . . . 8
                  
                    |
195 | | simpll 768 |
. . . . . . . . 9
                  
  |
196 | | simplrr 779 |
. . . . . . . . 9
                  
  
       |
197 | 190 | fnvinran 37398 |
. . . . . . . . 9
                  
 
      |
198 | | simp3 1032 |
. . . . . . . . . 10
 
  
                    |
199 | | nfv 1769 |
. . . . . . . . . . . . 13
         |
200 | 34, 36, 199 | nf3an 2033 |
. . . . . . . . . . . 12
   
               |
201 | | nfv 1769 |
. . . . . . . . . . . 12
                   |
202 | 200, 201 | nfim 2023 |
. . . . . . . . . . 11
                                     |
203 | | eleq1 2537 |
. . . . . . . . . . . . 13
                 |
204 | 203 | 3anbi3d 1371 |
. . . . . . . . . . . 12
        
  
     
                   |
205 | | fveq2 5879 |
. . . . . . . . . . . . 13
                       |
206 | | id 22 |
. . . . . . . . . . . . 13
               |
207 | 205, 206 | eleq12d 2543 |
. . . . . . . . . . . 12
           
                   |
208 | 204, 207 | imbi12d 327 |
. . . . . . . . . . 11
                                                             |
209 | 202, 208,
122 | vtoclg1f 3092 |
. . . . . . . . . 10
        
  
                               |
210 | 198, 209 | mpcom 36 |
. . . . . . . . 9
 
  
                              |
211 | 195, 196,
197, 210 | syl3anc 1292 |
. . . . . . . 8
                  
                  |
212 | 194, 211 | eqeltrd 2549 |
. . . . . . 7
                  
                |
213 | | fvco3 5957 |
. . . . . . . . . . . 12
              
 
              |
214 | 187, 213 | sylan 479 |
. . . . . . . . . . 11
 
                     |
215 | 187 | fnvinran 37398 |
. . . . . . . . . . . 12
 
           |
216 | 50 | adantr 472 |
. . . . . . . . . . . . 13
 
       |
217 | | rabexg 4549 |
. . . . . . . . . . . . 13
 
 
        
                             |
218 | 216, 217 | syl 17 |
. . . . . . . . . . . 12
 
     
 
        
                             |
219 | | raleq 2973 |
. . . . . . . . . . . . . . 15
      
   
 
               |
220 | 219 | 3anbi2d 1370 |
. . . . . . . . . . . . . 14
            
    

                  
 

         
          
                |
221 | 220 | rabbidv 3022 |
. . . . . . . . . . . . 13
     
 
        
                        

         
          
                |
222 | 221, 5 | fvmptg 5961 |
. . . . . . . . . . . 12
             
    
                                   
 
        
                             |
223 | 215, 218,
222 | syl2anc 673 |
. . . . . . . . . . 11
 
               
          
          
                |
224 | 214, 223 | eqtrd 2505 |
. . . . . . . . . 10
 
             
          
          
                |
225 | 224 | adantlr 729 |
. . . . . . . . 9
                  
 
           
    
                            |
226 | 225 | eleq2d 2534 |
. . . . . . . 8
                  
   
                          
    
                             |
227 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
228 | 24, 227 | nfco 5005 |
. . . . . . . . . . . . 13
     |
229 | 20, 228 | nfco 5005 |
. . . . . . . . . . . 12
   
   |
230 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
231 | 229, 230 | nffv 5886 |
. . . . . . . . . . 11
           |
232 | | nfcv 2612 |
. . . . . . . . . . 11
   |
233 | | nfcv 2612 |
. . . . . . . . . . . . 13
   |
234 | | nfcv 2612 |
. . . . . . . . . . . . . . 15
   |
235 | | nfcv 2612 |
. . . . . . . . . . . . . . 15
  |
236 | | nfcv 2612 |
. . . . . . . . . . . . . . . 16
   |
237 | 231, 236 | nffv 5886 |
. . . . . . . . . . . . . . 15
               |
238 | 234, 235,
237 | nfbr 4440 |
. . . . . . . . . . . . . 14
 
   
         |
239 | | nfcv 2612 |
. . . . . . . . . . . . . . 15
   |
240 | 237, 235,
239 | nfbr 4440 |
. . . . . . . . . . . . . 14
             
 |
241 | 238, 240 | nfan 2031 |
. . . . . . . . . . . . 13
                          
  |
242 | 233, 241 | nfral 2789 |
. . . . . . . . . . . 12
  
                        
  |
243 | | nfcv 2612 |
. . . . . . . . . . . . 13
       |
244 | | nfcv 2612 |
. . . . . . . . . . . . . 14
  |
245 | | nfcv 2612 |
. . . . . . . . . . . . . 14
     |
246 | 237, 244,
245 | nfbr 4440 |
. . . . . . . . . . . . 13
             
   |
247 | 243, 246 | nfral 2789 |
. . . . . . . . . . . 12
  
                
   |
248 | | nfcv 2612 |
. . . . . . . . . . . . 13
     |
249 | | nfcv 2612 |
. . . . . . . . . . . . . 14
       |
250 | 249, 244,
237 | nfbr 4440 |
. . . . . . . . . . . . 13
                   |
251 | 248, 250 | nfral 2789 |
. . . . . . . . . . . 12
  
                    |
252 | 242, 247,
251 | nf3an 2033 |
. . . . . . . . . . 11
                
   
        
                                          |
253 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
254 | | nfcv 2612 |
. . . . . . . . . . . . . . . 16
   |
255 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
256 | | nfra1 2785 |
. . . . . . . . . . . . . . . . . . . . 21
           
  |
257 | | nfra1 2785 |
. . . . . . . . . . . . . . . . . . . . 21
      
   |
258 | | nfra1 2785 |
. . . . . . . . . . . . . . . . . . . . 21
               |
259 | 256, 257,
258 | nf3an 2033 |
. . . . . . . . . . . . . . . . . . . 20
        
    

                    |
260 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . 20
   |
261 | 259, 260 | nfrab 2958 |
. . . . . . . . . . . . . . . . . . 19
  
 
          
     
               |
262 | 255, 261 | nfmpt 4484 |
. . . . . . . . . . . . . . . . . 18
     
          
     
                |
263 | 5, 262 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . 17
   |
264 | | nfcv 2612 |
. . . . . . . . . . . . . . . . 17
   |
265 | 263, 264 | nfco 5005 |
. . . . . . . . . . . . . . . 16
     |
266 | 254, 265 | nfco 5005 |
. . . . . . . . . . . . . . 15
   
   |
267 | | nfcv 2612 |
. . . . . . . . . . . . . . 15
   |
268 | 266, 267 | nffv 5886 |
. . . . . . . . . . . . . 14
           |
269 | 253, 268 | nfeq 2623 |
. . . . . . . . . . . . 13
          |
270 | | fveq1 5878 |
. . . . . . . . . . . . . . 15
                           |
271 | 270 | breq2d 4407 |
. . . . . . . . . . . . . 14
         
   
               |
272 | 270 | breq1d 4405 |
. . . . . . . . . . . . . 14
             
   
           |
273 | 271, 272 | anbi12d 725 |
. . . . . . . . . . . . 13
                  
                         
    |
274 | 269, 273 | ralbid 2826 |
. . . . . . . . . . . 12
          
        
 
                        
    |
275 | 270 | breq1d 4405 |
. . . . . . . . . . . . 13
             
 
   
             |
276 | 269, 275 | ralbid 2826 |
. . . . . . . . . . . 12
          
        
 
                       |
277 | 270 | breq2d 4407 |
. . . . . . . . . . . . 13
                 
                   |
278 | 269, 277 | ralbid 2826 |
. . . . . . . . . . . 12
          
          
                       |
279 | 274, 276,
278 | 3anbi123d 1365 |
. . . . . . . . . . 11
                
    
                        
 

   
                     
        
                                  |
280 | 231, 232,
252, 279 | elrabf 3182 |
. . . . . . . . . 10
   
       
          
          
             
   
    
 
                        
                                             |
281 | 280 | simprbi 471 |
. . . . . . . . 9
   
       
          
          
               
                        
                                            |
282 | 281 | simp2d 1043 |
. . . . . . . 8
   
       
          
          
                                    |
283 | 226, 282 | syl6bi 236 |
. . . . . . 7
                  
   
          
                       |
284 | 212, 283 | mpd 15 |
. . . . . 6
                  
                      |
285 | | stoweidlem31.2 |
. . . . . . . . 9
   |
286 | 263 | nfrn 5083 |
. . . . . . . . . . 11
   |
287 | 254, 286 | nffn 5682 |
. . . . . . . . . 10
  |
288 | | nfv 1769 |
. . . . . . . . . . 11
         |
289 | 286, 288 | nfral 2789 |
. . . . . . . . . 10
           |
290 | 287, 289 | nfan 2031 |
. . . . . . . . 9
     
       |
291 | 285, 290 | nfan 2031 |
. . . . . . . 8
               |
292 | | nfv 1769 |
. . . . . . . 8
      |
293 | 291, 292 | nfan 2031 |
. . . . . . 7
       
      
      |
294 | | stoweidlem31.11 |
. . . . . . . . . . 11

    |
295 | 294 | ad3antrrr 744 |
. . . . . . . . . 10
       
      
     
    |
296 | | simpr 468 |
. . . . . . . . . 10
       
      
     
  |
297 | 295, 296 | sseldd 3419 |
. . . . . . . . 9
       
      
     

   |
298 | 281 | simp3d 1044 |
. . . . . . . . . . . 12
   
       
          
          
                                    |
299 | 226, 298 | syl6bi 236 |
. . . . . . . . . . 11
                  
   
          
                       |
300 | 212, 299 | mpd 15 |
. . . . . . . . . 10
                  
                      |
301 | 300 | r19.21bi 2776 |
. . . . . . . . 9
       
      
       
                  |
302 | 297, 301 | syldan 478 |
. . . . . . . 8
       
      
     
                  |
303 | 302 | ex 441 |
. . . . . . 7
                  

                   |
304 | 293, 303 | ralrimi 2800 |
. . . . . 6
                  

                  |
305 | 284, 304 | jca 541 |
. . . . 5
                  
 
        
                              |
306 | 305 | ralrimiva 2809 |
. . . 4
 
 
                                                        |
307 | 192, 306 | jca 541 |
. . 3
 
 
                      
                       
  
                    |
308 | | feq1 5720 |
. . . . 5
               
             |
309 | | nfcv 2612 |
. . . . . . . . 9
   |
310 | 309, 266 | nfeq 2623 |
. . . . . . . 8
      |
311 | | fveq1 5878 |
. . . . . . . . . 10
                   |
312 | 311 | fveq1d 5881 |
. . . . . . . . 9
                           |
313 | 312 | breq1d 4405 |
. . . . . . . 8
             
 
   
             |
314 | 310, 313 | ralbid 2826 |
. . . . . . 7
      
            
 
                       |
315 | 312 | breq2d 4407 |
. . . . . . . 8
                 
                   |
316 | 310, 315 | ralbid 2826 |
. . . . . . 7
      
           

                   |
317 | 314, 316 | anbi12d 725 |
. . . . . 6
                                    
 
        ![]() |