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

  |
8 | 6, 7 | ssexd 4550 |
. . . . . . . 8
   |
9 | | mptexg 6135 |
. . . . . . . 8
         
    

                       |
10 | 8, 9 | syl 17 |
. . . . . . 7
    
          
     
                 |
11 | 5, 10 | syl5eqel 2533 |
. . . . . 6
   |
12 | | vex 3048 |
. . . . . 6
 |
13 | | coexg 6744 |
. . . . . 6
 
     |
14 | 11, 12, 13 | sylancl 668 |
. . . . 5
     |
15 | | coexg 6744 |
. . . . 5
  
   
    |
16 | 4, 14, 15 | sylancr 669 |
. . . 4
  
    |
17 | 16 | adantr 467 |
. . 3
 
 
               |
18 | | simprl 764 |
. . . . . 6
 
 
           |
19 | | stoweidlem31.1 |
. . . . . . . . 9
   |
20 | | nfcv 2592 |
. . . . . . . . . . 11
   |
21 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
22 | | nfrab1 2971 |
. . . . . . . . . . . . . 14
  
 
          
     
               |
23 | 21, 22 | nfmpt 4491 |
. . . . . . . . . . . . 13
     
          
     
                |
24 | 5, 23 | nfcxfr 2590 |
. . . . . . . . . . . 12
   |
25 | 24 | nfrn 5077 |
. . . . . . . . . . 11
   |
26 | 20, 25 | nffn 5672 |
. . . . . . . . . 10

 |
27 | | nfv 1761 |
. . . . . . . . . . 11
         |
28 | 25, 27 | nfral 2774 |
. . . . . . . . . 10
  
        |
29 | 26, 28 | nfan 2011 |
. . . . . . . . 9
     
       |
30 | 19, 29 | nfan 2011 |
. . . . . . . 8
  
            |
31 | | fvelrnb 5912 |
. . . . . . . . . . . . 13
           |
32 | 18, 31 | syl 17 |
. . . . . . . . . . . 12
 
 
         
         |
33 | 32 | biimpa 487 |
. . . . . . . . . . 11
                       |
34 | | nfv 1761 |
. . . . . . . . . . . . . 14
   |
35 | | nfv 1761 |
. . . . . . . . . . . . . . 15
  |
36 | | nfra1 2769 |
. . . . . . . . . . . . . . 15
           |
37 | 35, 36 | nfan 2011 |
. . . . . . . . . . . . . 14
     
       |
38 | 34, 37 | nfan 2011 |
. . . . . . . . . . . . 13
               |
39 | | nfv 1761 |
. . . . . . . . . . . . 13
  |
40 | 38, 39 | nfan 2011 |
. . . . . . . . . . . 12
       
      
  |
41 | | simp3 1010 |
. . . . . . . . . . . . . 14
       
      
     
      |
42 | | simp1ll 1071 |
. . . . . . . . . . . . . . 15
       
      
     
  |
43 | | simplrr 771 |
. . . . . . . . . . . . . . . 16
                 
       |
44 | 43 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . 15
       
      
     
  
       |
45 | | simp2 1009 |
. . . . . . . . . . . . . . 15
       
      
     
  |
46 | | simp3 1010 |
. . . . . . . . . . . . . . . . 17
 
  
        |
47 | | 3simpc 1007 |
. . . . . . . . . . . . . . . . . 18
 
  
         
        |
48 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
49 | | stoweidlem31.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
50 | | stoweidlem31.13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
51 | | rabexg 4553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 
        
                        |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
          
     
                |
53 | 52 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
          
     
                 |
54 | 49, 53 | ralrimi 2788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
 
          
     
                |
55 | 5 | fnmpt 5704 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       
    

                      |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
57 | 56 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
58 | | fvelrnb 5912 |
. . . . . . . . . . . . . . . . . . . . . . 23
          |
59 | | nfmpt1 4492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
          
     
                |
60 | 5, 59 | nfcxfr 2590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
61 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
62 | 60, 61 | nffv 5872 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
63 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
64 | 62, 63 | nfeq 2603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
65 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
66 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
67 | 66 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
68 | 64, 65, 67 | cbvrex 3016 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

      |
69 | 58, 68 | syl6bb 265 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
70 | 57, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
          |
71 | 48, 70 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . 20
 
 
      |
72 | 60 | nfrn 5077 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
73 | 72 | nfcri 2586 |
. . . . . . . . . . . . . . . . . . . . . 22

 |
74 | 49, 73 | nfan 2011 |
. . . . . . . . . . . . . . . . . . . . 21
  
  |
75 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . 21
  |
76 | | simp3 1010 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
      |
77 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
78 | 50 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
79 | 78, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 
 
        
                        |
80 | 5 | fvmpt2 5957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
    

                         
 
        
                        |
81 | 77, 79, 80 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       
          
     
                |
82 | 7 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
83 | | stoweidlem31.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             
           
       |
84 | 83 | rabeq2i 3042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30


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

         
                  |
86 | 85 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    
          
                 |
87 | | stoweidlem31.10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
88 | | stoweidlem31.8 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
89 | 88 | nnrpd 11339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
90 | 87, 89 | rpdivcld 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
91 | 90 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
     |
92 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       
         |
93 | 92 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
   

         |
94 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
95 | 94 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
   
           |
96 | 95 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
        
               |
97 | 93, 96 | 3anbi23d 1342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
    

         
    
 

         
     
                |
98 | 97 | rexbidv 2901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
          
           
    

 

         
     
                |
99 | 98 | rspccva 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
              
           
     
             
                       |
100 | 86, 91, 99 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 
 

         
     
               |
101 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

 |
102 | 19, 101 | nfan 2011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
  |
103 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
104 | 22, 103 | nfne 2723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
 
          
     
               |
105 | | 3simpc 1007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 
        
                        

         
     
                |
106 | | rabid 2967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   

         
     
             

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

                      |
108 | | ne0i 3737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   

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

         
     
                |
110 | 109 | 3exp 1207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    
          
     
            

 
        
                          |
111 | 102, 104,
110 | rexlimd 2871 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
          
                     
 
          
     
                 |
112 | 100, 111 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 
 
        
                        |
113 | 81, 112 | eqnetrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
114 | 113 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
      |
115 | 76, 114 | eqnetrrd 2692 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
  |
116 | 115 | 3adant1r 1261 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       |
117 | 116 | 3exp 1207 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
118 | 74, 75, 117 | rexlimd 2871 |
. . . . . . . . . . . . . . . . . . . 20
 
  
       |
119 | 71, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
 
   |
120 | 119 | 3adant2 1027 |
. . . . . . . . . . . . . . . . . 18
 
  
        |
121 | | rspa 2755 |
. . . . . . . . . . . . . . . . . 18
                   |
122 | 47, 120, 121 | sylc 62 |
. . . . . . . . . . . . . . . . 17
 
  
            |
123 | 46, 122 | jca 535 |
. . . . . . . . . . . . . . . 16
 
  
              |
124 | | vex 3048 |
. . . . . . . . . . . . . . . . . 18
 |
125 | 5 | elrnmpt 5081 |
. . . . . . . . . . . . . . . . . 18
     

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



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

 
        
                        |
128 | | nfv 1761 |
. . . . . . . . . . . . . . . . . 18
       |
129 | 73, 128 | nfan 2011 |
. . . . . . . . . . . . . . . . 17
         |
130 | | nfv 1761 |
. . . . . . . . . . . . . . . . 17
       |
131 | | simp1r 1033 |
. . . . . . . . . . . . . . . . . . 19
          
          
     
                     |
132 | | simp3 1010 |
. . . . . . . . . . . . . . . . . . 19
          
          
     
               
 
        
                        |
133 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . 22
     

 
        
                      
      |
134 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
     

 
        
                      

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

 
        
                      
           
    

                      |
136 | | elrabi 3193 |
. . . . . . . . . . . . . . . . . . . . . 22
       

         
     
                    |
137 | | fveq1 5864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
138 | 137 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
   
           |
139 | 137 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
           |
140 | 138, 139 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
              
                 
    |
141 | 140 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
        
 
                
    |
142 | 137 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
 
             |
143 | 142 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
   
 

             |
144 | 137 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             
               |
145 | 144 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
          
                   |
146 | 141, 143,
145 | 3anbi123d 1339 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
    

                  
 

                 
         
                    |
147 | 146 | elrab 3196 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       

         
     
             
    
 
                
                                |
148 | 147 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
       

         
     
               
                
                               |
149 | 148 | simp1d 1020 |
. . . . . . . . . . . . . . . . . . . . . 22
       

         
     
              
                    |
150 | 141 | elrab 3196 |
. . . . . . . . . . . . . . . . . . . . . 22
      
          
    

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

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

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

 
        
                      
      |
155 | 131, 132,
154 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
          
          
     
                     |
156 | 155 | 3exp 1207 |
. . . . . . . . . . . . . . . . 17
       
   
          
     
                      |
157 | 129, 130,
156 | rexlimd 2871 |
. . . . . . . . . . . . . . . 16
        

 
          
     
                     |
158 | 123, 127,
157 | sylc 62 |
. . . . . . . . . . . . . . 15
 
  
            |
159 | 42, 44, 45, 158 | syl3anc 1268 |
. . . . . . . . . . . . . 14
       
      
     
      |
160 | 41, 159 | eqeltrrd 2530 |
. . . . . . . . . . . . 13
       
      
     
  |
161 | 160 | 3exp 1207 |
. . . . . . . . . . . 12
                         |
162 | 40, 161 | reximdai 2856 |
. . . . . . . . . . 11
                
     
   |
163 | 33, 162 | mpd 15 |
. . . . . . . . . 10
                  |
164 | | nfv 1761 |
. . . . . . . . . . 11
  |
165 | | idd 25 |
. . . . . . . . . . . 12
     |
166 | 165 | a1i 11 |
. . . . . . . . . . 11
                     |
167 | 40, 164, 166 | rexlimd 2871 |
. . . . . . . . . 10
                
   |
168 | 163, 167 | mpd 15 |
. . . . . . . . 9
                 |
169 | 168 | ex 436 |
. . . . . . . 8
 
 
             |
170 | 30, 169 | ralrimi 2788 |
. . . . . . 7
 
 
         
  |
171 | | dfss3 3422 |
. . . . . . . 8

   |
172 | | nfrab1 2971 |
. . . . . . . . . . 11
  
         
   |
173 | 153, 172 | nfcxfr 2590 |
. . . . . . . . . 10
   |
174 | 173 | nfcri 2586 |
. . . . . . . . 9

 |
175 | | nfv 1761 |
. . . . . . . . 9
  |
176 | | eleq1 2517 |
. . . . . . . . 9
 
   |
177 | 174, 175,
176 | cbvral 3015 |
. . . . . . . 8
 
   |
178 | 171, 177 | bitri 253 |
. . . . . . 7

   |
179 | 170, 178 | sylibr 216 |
. . . . . 6
 
 
        
  |
180 | | df-f 5586 |
. . . . . 6
    
    |
181 | 18, 179, 180 | sylanbrc 670 |
. . . . 5
 
 
               |
182 | | dffn3 5736 |
. . . . . . . 8

      |
183 | 56, 182 | sylib 200 |
. . . . . . 7
       |
184 | 183 | adantr 467 |
. . . . . 6
 
 
               |
185 | | stoweidlem31.9 |
. . . . . . . 8
           |
186 | | f1of 5814 |
. . . . . . . 8
        
          |
187 | 185, 186 | syl 17 |
. . . . . . 7
           |
188 | 187 | adantr 467 |
. . . . . 6
 
 
                   |
189 | | fco 5739 |
. . . . . 6
              
            |
190 | 184, 188,
189 | syl2anc 667 |
. . . . 5
 
 
                     |
191 | | fco 5739 |
. . . . 5
                  
            |
192 | 181, 190,
191 | syl2anc 667 |
. . . 4
 
 
                       |
193 | | fvco3 5942 |
. . . . . . . . 9
           
       
                 |
194 | 190, 193 | sylan 474 |
. . . . . . . 8
                  
                    |
195 | | simpll 760 |
. . . . . . . . 9
                  
  |
196 | | simplrr 771 |
. . . . . . . . 9
                  
  
       |
197 | 190 | fnvinran 37335 |
. . . . . . . . 9
                  
 
      |
198 | | simp3 1010 |
. . . . . . . . . 10
 
  
                    |
199 | | nfv 1761 |
. . . . . . . . . . . . 13
         |
200 | 34, 36, 199 | nf3an 2013 |
. . . . . . . . . . . 12
   
               |
201 | | nfv 1761 |
. . . . . . . . . . . 12
                   |
202 | 200, 201 | nfim 2003 |
. . . . . . . . . . 11
                                     |
203 | | eleq1 2517 |
. . . . . . . . . . . . 13
                 |
204 | 203 | 3anbi3d 1345 |
. . . . . . . . . . . 12
        
  
     
                   |
205 | | fveq2 5865 |
. . . . . . . . . . . . 13
                       |
206 | | id 22 |
. . . . . . . . . . . . 13
               |
207 | 205, 206 | eleq12d 2523 |
. . . . . . . . . . . 12
           
                   |
208 | 204, 207 | imbi12d 322 |
. . . . . . . . . . 11
                                                             |
209 | 202, 208,
122 | vtoclg1f 3106 |
. . . . . . . . . 10
        
  
                               |
210 | 198, 209 | mpcom 37 |
. . . . . . . . 9
 
  
                              |
211 | 195, 196,
197, 210 | syl3anc 1268 |
. . . . . . . 8
                  
                  |
212 | 194, 211 | eqeltrd 2529 |
. . . . . . 7
                  
                |
213 | | fvco3 5942 |
. . . . . . . . . . . 12
              
 
              |
214 | 187, 213 | sylan 474 |
. . . . . . . . . . 11
 
                     |
215 | 187 | fnvinran 37335 |
. . . . . . . . . . . 12
 
           |
216 | 50 | adantr 467 |
. . . . . . . . . . . . 13
 
       |
217 | | rabexg 4553 |
. . . . . . . . . . . . 13
 
 
        
                             |
218 | 216, 217 | syl 17 |
. . . . . . . . . . . 12
 
     
 
        
                             |
219 | | raleq 2987 |
. . . . . . . . . . . . . . 15
      
   
 
               |
220 | 219 | 3anbi2d 1344 |
. . . . . . . . . . . . . 14
            
    

                  
 

         
          
                |
221 | 220 | rabbidv 3036 |
. . . . . . . . . . . . 13
     
 
        
                        

         
          
                |
222 | 221, 5 | fvmptg 5946 |
. . . . . . . . . . . 12
             
    
                                   
 
        
                             |
223 | 215, 218,
222 | syl2anc 667 |
. . . . . . . . . . 11
 
               
          
          
                |
224 | 214, 223 | eqtrd 2485 |
. . . . . . . . . 10
 
             
          
          
                |
225 | 224 | adantlr 721 |
. . . . . . . . 9
                  
 
           
    
                            |
226 | 225 | eleq2d 2514 |
. . . . . . . 8
                  
   
                          
    
                             |
227 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
228 | 24, 227 | nfco 5000 |
. . . . . . . . . . . . 13
     |
229 | 20, 228 | nfco 5000 |
. . . . . . . . . . . 12
   
   |
230 | | nfcv 2592 |
. . . . . . . . . . . 12
   |
231 | 229, 230 | nffv 5872 |
. . . . . . . . . . 11
           |
232 | | nfcv 2592 |
. . . . . . . . . . 11
   |
233 | | nfcv 2592 |
. . . . . . . . . . . . 13
   |
234 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
235 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
  |
236 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
   |
237 | 231, 236 | nffv 5872 |
. . . . . . . . . . . . . . 15
               |
238 | 234, 235,
237 | nfbr 4447 |
. . . . . . . . . . . . . 14
 
   
         |
239 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
240 | 237, 235,
239 | nfbr 4447 |
. . . . . . . . . . . . . 14
             
 |
241 | 238, 240 | nfan 2011 |
. . . . . . . . . . . . 13
                          
  |
242 | 233, 241 | nfral 2774 |
. . . . . . . . . . . 12
  
                        
  |
243 | | nfcv 2592 |
. . . . . . . . . . . . 13
       |
244 | | nfcv 2592 |
. . . . . . . . . . . . . 14
  |
245 | | nfcv 2592 |
. . . . . . . . . . . . . 14
     |
246 | 237, 244,
245 | nfbr 4447 |
. . . . . . . . . . . . 13
             
   |
247 | 243, 246 | nfral 2774 |
. . . . . . . . . . . 12
  
                
   |
248 | | nfcv 2592 |
. . . . . . . . . . . . 13
     |
249 | | nfcv 2592 |
. . . . . . . . . . . . . 14
       |
250 | 249, 244,
237 | nfbr 4447 |
. . . . . . . . . . . . 13
                   |
251 | 248, 250 | nfral 2774 |
. . . . . . . . . . . 12
  
                    |
252 | 242, 247,
251 | nf3an 2013 |
. . . . . . . . . . 11
                
   
        
                                          |
253 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
254 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
   |
255 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . 19
   |
256 | | nfra1 2769 |
. . . . . . . . . . . . . . . . . . . . 21
           
  |
257 | | nfra1 2769 |
. . . . . . . . . . . . . . . . . . . . 21
      
   |
258 | | nfra1 2769 |
. . . . . . . . . . . . . . . . . . . . 21
               |
259 | 256, 257,
258 | nf3an 2013 |
. . . . . . . . . . . . . . . . . . . 20
        
    

                    |
260 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . 20
   |
261 | 259, 260 | nfrab 2972 |
. . . . . . . . . . . . . . . . . . 19
  
 
          
     
               |
262 | 255, 261 | nfmpt 4491 |
. . . . . . . . . . . . . . . . . 18
     
          
     
                |
263 | 5, 262 | nfcxfr 2590 |
. . . . . . . . . . . . . . . . 17
   |
264 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
   |
265 | 263, 264 | nfco 5000 |
. . . . . . . . . . . . . . . 16
     |
266 | 254, 265 | nfco 5000 |
. . . . . . . . . . . . . . 15
   
   |
267 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
268 | 266, 267 | nffv 5872 |
. . . . . . . . . . . . . 14
           |
269 | 253, 268 | nfeq 2603 |
. . . . . . . . . . . . 13
          |
270 | | fveq1 5864 |
. . . . . . . . . . . . . . 15
                           |
271 | 270 | breq2d 4414 |
. . . . . . . . . . . . . 14
         
   
               |
272 | 270 | breq1d 4412 |
. . . . . . . . . . . . . 14
             
   
           |
273 | 271, 272 | anbi12d 717 |
. . . . . . . . . . . . 13
                  
                         
    |
274 | 269, 273 | ralbid 2822 |
. . . . . . . . . . . 12
          
        
 
                        
    |
275 | 270 | breq1d 4412 |
. . . . . . . . . . . . 13
             
 
   
             |
276 | 269, 275 | ralbid 2822 |
. . . . . . . . . . . 12
          
        
 
                       |
277 | 270 | breq2d 4414 |
. . . . . . . . . . . . 13
                 
                   |
278 | 269, 277 | ralbid 2822 |
. . . . . . . . . . . 12
          
          
                       |
279 | 274, 276,
278 | 3anbi123d 1339 |
. . . . . . . . . . 11
                
    
                        
 

   
                     
        
                                  |
280 | 231, 232,
252, 279 | elrabf 3194 |
. . . . . . . . . 10
   
       
          
          
             
   
    
 
                        
                                             |
281 | 280 | simprbi 466 |
. . . . . . . . 9
   
       
          
          
               
                        
                                            |
282 | 281 | simp2d 1021 |
. . . . . . . 8
   
       
          
          
                                    |
283 | 226, 282 | syl6bi 232 |
. . . . . . 7
                  
   
          
                       |
284 | 212, 283 | mpd 15 |
. . . . . 6
                  
                      |
285 | | stoweidlem31.2 |
. . . . . . . . 9
   |
286 | 263 | nfrn 5077 |
. . . . . . . . . . 11
   |
287 | 254, 286 | nffn 5672 |
. . . . . . . . . 10
  |
288 | | nfv 1761 |
. . . . . . . . . . 11
         |
289 | 286, 288 | nfral 2774 |
. . . . . . . . . 10
           |
290 | 287, 289 | nfan 2011 |
. . . . . . . . 9
     
       |
291 | 285, 290 | nfan 2011 |
. . . . . . . 8
               |
292 | | nfv 1761 |
. . . . . . . 8
      |
293 | 291, 292 | nfan 2011 |
. . . . . . 7
       
      
      |
294 | | stoweidlem31.11 |
. . . . . . . . . . 11

    |
295 | 294 | ad3antrrr 736 |
. . . . . . . . . 10
       
      
     
    |
296 | | simpr 463 |
. . . . . . . . . 10
       
      
     
  |
297 | 295, 296 | sseldd 3433 |
. . . . . . . . 9
       
      
     

   |
298 | 281 | simp3d 1022 |
. . . . . . . . . . . 12
   
       
          
          
                                    |
299 | 226, 298 | syl6bi 232 |
. . . . . . . . . . 11
                  
   
          
                       |
300 | 212, 299 | mpd 15 |
. . . . . . . . . 10
                  
                      |
301 | 300 | r19.21bi 2757 |
. . . . . . . . 9
       
      
       
                  |
302 | 297, 301 | syldan 473 |
. . . . . . . 8
       
      
     
                  |
303 | 302 | ex 436 |
. . . . . . 7
                  

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

                  |
305 | 284, 304 | jca 535 |
. . . . 5
                  
 
        
                              |
306 | 305 | ralrimiva 2802 |
. . . 4
 
 
                                                        |
307 | 192, 306 | jca 535 |
. . 3
 
 
                      
                       
  
                    |
308 | | feq1 5710 |
. . . . 5
               
             |
309 | | nfcv 2592 |
. . . . . . . . 9
   |
310 | 309, 266 | nfeq 2603 |
. . . . . . . 8
      |
311 | | fveq1 5864 |
. . . . . . . . . 10
                   |
312 | 311 | fveq1d 5867 |
. . . . . . . . 9
                           |
313 | 312 | breq1d 4412 |
. . . . . . . 8
             
 
   
             |
314 | 310, 313 | ralbid 2822 |
. . . . . . 7
      
            
 
                       |
315 | 312 | breq2d 4414 |
. . . . . . . 8
                 
                   |
316 | 310, 315 | ralbid 2822 |
. . . . . . 7
      
           

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