Step | Hyp | Ref
| Expression |
1 | | locfinref.4 |
. . . 4
     |
2 | | locfinref.5 |
. . . . 5
       |
3 | | reff 28740 |
. . . . 5
    
             
         |
4 | 2, 3 | syl 17 |
. . . 4
                        |
5 | 1, 4 | mpbid 215 |
. . 3
                    |
6 | 5 | simprd 470 |
. 2
                |
7 | | funmpt 5625 |
. . . . . 6
           |
8 | 7 | a1i 11 |
. . . . 5
                          |
9 | | eqid 2471 |
. . . . . . 7
                     |
10 | 9 | dmmptss 5338 |
. . . . . 6
           |
11 | | frn 5747 |
. . . . . . 7
    
  |
12 | 11 | ad2antlr 741 |
. . . . . 6
             
  |
13 | 10, 12 | syl5ss 3429 |
. . . . 5
                          |
14 | | locfintop 20613 |
. . . . . . . . . 10
    
  |
15 | 2, 14 | syl 17 |
. . . . . . . . 9
   |
16 | 15 | ad3antrrr 744 |
. . . . . . . 8
              
   |
17 | | cnvimass 5194 |
. . . . . . . . . 10
        |
18 | | fdm 5745 |
. . . . . . . . . . 11
    
  |
19 | 18 | ad3antlr 745 |
. . . . . . . . . 10
              

  |
20 | 17, 19 | syl5sseq 3466 |
. . . . . . . . 9
              
          |
21 | | locfinref.3 |
. . . . . . . . . 10

  |
22 | 21 | ad3antrrr 744 |
. . . . . . . . 9
              
   |
23 | 20, 22 | sstrd 3428 |
. . . . . . . 8
              
          |
24 | | uniopn 20004 |
. . . . . . . 8
                    |
25 | 16, 23, 24 | syl2anc 673 |
. . . . . . 7
              
           |
26 | 25 | ralrimiva 2809 |
. . . . . 6
              
           |
27 | 9 | rnmptss 6068 |
. . . . . 6
 
        
         
  |
28 | 26, 27 | syl 17 |
. . . . 5
                          |
29 | | eqid 2471 |
. . . . . . . . . 10
   |
30 | | eqid 2471 |
. . . . . . . . . 10
   |
31 | 29, 30 | refbas 20602 |
. . . . . . . . 9
       |
32 | 1, 31 | syl 17 |
. . . . . . . 8
     |
33 | 32 | ad2antrr 740 |
. . . . . . 7
              
   |
34 | | nfv 1769 |
. . . . . . . . . . . . 13
         |
35 | | nfra1 2785 |
. . . . . . . . . . . . 13
        |
36 | 34, 35 | nfan 2031 |
. . . . . . . . . . . 12
                |
37 | | nfre1 2846 |
. . . . . . . . . . . 12
  
 |
38 | 36, 37 | nfan 2031 |
. . . . . . . . . . 11
               

  |
39 | | ffn 5739 |
. . . . . . . . . . . . . . 15
       |
40 | 39 | ad4antlr 747 |
. . . . . . . . . . . . . 14
               
    |
41 | | simplr 770 |
. . . . . . . . . . . . . 14
               
    |
42 | | fnfvelrn 6034 |
. . . . . . . . . . . . . 14
 
       |
43 | 40, 41, 42 | syl2anc 673 |
. . . . . . . . . . . . 13
               
        |
44 | | ssid 3437 |
. . . . . . . . . . . . . . 15
 |
45 | 39 | ad3antlr 745 |
. . . . . . . . . . . . . . . 16
              
   |
46 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
         |
47 | | fniniseg 6018 |
. . . . . . . . . . . . . . . . . 18
            

            |
48 | 47 | biimpar 493 |
. . . . . . . . . . . . . . . . 17
            
             |
49 | 46, 48 | mpanr2 698 |
. . . . . . . . . . . . . . . 16
 
              |
50 | 45, 49 | sylancom 680 |
. . . . . . . . . . . . . . 15
              
              |
51 | | ssuni 4212 |
. . . . . . . . . . . . . . 15
 
                          |
52 | 44, 50, 51 | sylancr 676 |
. . . . . . . . . . . . . 14
              
               |
53 | 52 | sselda 3418 |
. . . . . . . . . . . . 13
               
                |
54 | | sneq 3969 |
. . . . . . . . . . . . . . . . 17
      
        |
55 | 54 | imaeq2d 5174 |
. . . . . . . . . . . . . . . 16
                         |
56 | 55 | unieqd 4200 |
. . . . . . . . . . . . . . 15
                           |
57 | 56 | eleq2d 2534 |
. . . . . . . . . . . . . 14
             
               |
58 | 57 | rspcev 3136 |
. . . . . . . . . . . . 13
     
             
          |
59 | 43, 53, 58 | syl2anc 673 |
. . . . . . . . . . . 12
               
             |
60 | 59 | adantllr 733 |
. . . . . . . . . . 11
     
     
     
              |
61 | | simpr 468 |
. . . . . . . . . . 11
              

 
  |
62 | 38, 60, 61 | r19.29af 2916 |
. . . . . . . . . 10
              

            |
63 | | nfv 1769 |
. . . . . . . . . . . . . 14
  |
64 | 36, 63 | nfan 2031 |
. . . . . . . . . . . . 13
               
  |
65 | | nfv 1769 |
. . . . . . . . . . . . 13
          |
66 | 64, 65 | nfan 2031 |
. . . . . . . . . . . 12
     
     
     
          |
67 | 20 | ad3antrrr 744 |
. . . . . . . . . . . . 13
                 
                  
      
  |
68 | | simplr 770 |
. . . . . . . . . . . . 13
                 
                  
         |
69 | 67, 68 | sseldd 3419 |
. . . . . . . . . . . 12
                 
                  
  |
70 | | simpr 468 |
. . . . . . . . . . . 12
                 
                  
  |
71 | | simpr 468 |
. . . . . . . . . . . . 13
               
                    |
72 | | eluni2 4194 |
. . . . . . . . . . . . 13
        
           |
73 | 71, 72 | sylib 201 |
. . . . . . . . . . . 12
               
                     |
74 | 66, 69, 70, 73 | reximd2a 2854 |
. . . . . . . . . . 11
               
          
  |
75 | 74 | r19.29an 2917 |
. . . . . . . . . 10
              
          
  |
76 | 62, 75 | impbida 850 |
. . . . . . . . 9
                
           |
77 | | eluni2 4194 |
. . . . . . . . 9
 

  |
78 | | eliun 4274 |
. . . . . . . . 9
          
           |
79 | 76, 77, 78 | 3bitr4g 296 |
. . . . . . . 8
                             |
80 | 79 | eqrdv 2469 |
. . . . . . 7
              

           |
81 | | dfiun3g 5093 |
. . . . . . . 8
 
        
          
            |
82 | 26, 81 | syl 17 |
. . . . . . 7
              
          
           |
83 | 33, 80, 82 | 3eqtrd 2509 |
. . . . . 6
              
             |
84 | 11 | ad3antlr 745 |
. . . . . . . . 9
              
          
  |
85 | | vex 3034 |
. . . . . . . . . . 11
 |
86 | 9 | elrnmpt 5087 |
. . . . . . . . . . 11
           
            |
87 | 85, 86 | mp1i 13 |
. . . . . . . . . 10
               
        
            |
88 | 87 | biimpa 492 |
. . . . . . . . 9
              
           
          |
89 | | ssrexv 3480 |
. . . . . . . . 9

 
        
           |
90 | 84, 88, 89 | sylc 61 |
. . . . . . . 8
              
           
          |
91 | | nfv 1769 |
. . . . . . . . . 10
                |
92 | | nfmpt1 4485 |
. . . . . . . . . . . 12
             |
93 | 92 | nfrn 5083 |
. . . . . . . . . . 11
             |
94 | 93 | nfcri 2606 |
. . . . . . . . . 10

           |
95 | 91, 94 | nfan 2031 |
. . . . . . . . 9
               
            |
96 | | simpr 468 |
. . . . . . . . . . 11
     
     
                                    |
97 | | nfv 1769 |
. . . . . . . . . . . . . . . 16
            |
98 | 36, 97 | nfan 2031 |
. . . . . . . . . . . . . . 15
               
            |
99 | | nfv 1769 |
. . . . . . . . . . . . . . 15
  |
100 | 98, 99 | nfan 2031 |
. . . . . . . . . . . . . 14
     
     
                  |
101 | | nfv 1769 |
. . . . . . . . . . . . . 14
          |
102 | 100, 101 | nfan 2031 |
. . . . . . . . . . . . 13
                 
                      |
103 | | simp-5r 787 |
. . . . . . . . . . . . . . . 16
                 
                            

      |
104 | 39 | ad5antlr 749 |
. . . . . . . . . . . . . . . . . . 19
     
     
                            |
105 | | fniniseg 6018 |
. . . . . . . . . . . . . . . . . . 19
        

        |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     
     
                                 

        |
107 | 106 | biimpa 492 |
. . . . . . . . . . . . . . . . 17
                 
                            

       |
108 | 107 | simpld 466 |
. . . . . . . . . . . . . . . 16
                 
                            
  |
109 | | rspa 2774 |
. . . . . . . . . . . . . . . 16
              |
110 | 103, 108,
109 | syl2anc 673 |
. . . . . . . . . . . . . . 15
                 
                            
      |
111 | 107 | simprd 470 |
. . . . . . . . . . . . . . 15
                 
                            
      |
112 | 110, 111 | sseqtrd 3454 |
. . . . . . . . . . . . . 14
                 
                            
  |
113 | 112 | ex 441 |
. . . . . . . . . . . . 13
     
     
                                     |
114 | 102, 113 | ralrimi 2800 |
. . . . . . . . . . . 12
     
     
                                  
  |
115 | | unissb 4221 |
. . . . . . . . . . . 12
                    |
116 | 114, 115 | sylibr 217 |
. . . . . . . . . . 11
     
     
                                    |
117 | 96, 116 | eqsstrd 3452 |
. . . . . . . . . 10
     
     
                            |
118 | 117 | exp31 615 |
. . . . . . . . 9
              
                         |
119 | 95, 118 | reximdai 2853 |
. . . . . . . 8
              
                     
   |
120 | 90, 119 | mpd 15 |
. . . . . . 7
              
           
  |
121 | 120 | ralrimiva 2809 |
. . . . . 6
              

          
  |
122 | | vex 3034 |
. . . . . . . . . 10
 |
123 | 122 | rnex 6746 |
. . . . . . . . 9
 |
124 | 123 | mptex 6152 |
. . . . . . . 8
           |
125 | | rnexg 6744 |
. . . . . . . 8
                       |
126 | 124, 125 | mp1i 13 |
. . . . . . 7
                          |
127 | | eqid 2471 |
. . . . . . . 8
 
                     |
128 | 127, 30 | isref 20601 |
. . . . . . 7
                       
 
           
                |
129 | 126, 128 | syl 17 |
. . . . . 6
              
           
 
           
                |
130 | 83, 121, 129 | mpbir2and 936 |
. . . . 5
                            |
131 | 15 | ad2antrr 740 |
. . . . . 6
             
  |
132 | | locfinref.2 |
. . . . . . . 8
    |
133 | 132 | ad2antrr 740 |
. . . . . . 7
             
   |
134 | 133, 83 | eqtrd 2505 |
. . . . . 6
             
             |
135 | | nfv 1769 |
. . . . . . . . 9
  |
136 | 36, 135 | nfan 2031 |
. . . . . . . 8
               
  |
137 | | simplr 770 |
. . . . . . . 8
     
     
                |
138 | | ffun 5742 |
. . . . . . . . . . . . . 14
       |
139 | 138 | ad6antlr 751 |
. . . . . . . . . . . . 13
                 


     
  |
140 | | imafi 7885 |
. . . . . . . . . . . . 13
      
          |
141 | 139, 140 | sylancom 680 |
. . . . . . . . . . . 12
                 


     
          |
142 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . 19
                  
       
              
                |
143 | | sneq 3969 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
144 | 143 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
145 | 144 | unieqd 4200 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
146 | 122 | cnvex 6759 |
. . . . . . . . . . . . . . . . . . . . . . 23
  |
147 | | imaexg 6749 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
148 | 146, 147 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
149 | 148 | uniex 6606 |
. . . . . . . . . . . . . . . . . . . . 21
         |
150 | 145, 9, 149 | fvmpt 5963 |
. . . . . . . . . . . . . . . . . . . 20
                         |
151 | 150 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . 19
                  
       
              
                        |
152 | 142, 151 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
                  
       
              
          |
153 | 152 | ineq1d 3624 |
. . . . . . . . . . . . . . . . 17
                  
       
              
              |
154 | 153 | neeq1d 2702 |
. . . . . . . . . . . . . . . 16
                  
       
              
 
              |
155 | 123 | a1i 11 |
. . . . . . . . . . . . . . . 16
                 


     
  |
156 | | imaexg 6749 |
. . . . . . . . . . . . . . . . . . . . 21
           |
157 | 146, 156 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
        |
158 | 157 | uniex 6606 |
. . . . . . . . . . . . . . . . . . 19
         |
159 | 158, 9 | fnmpti 5716 |
. . . . . . . . . . . . . . . . . 18
           |
160 | | dffn4 5812 |
. . . . . . . . . . . . . . . . . 18
                                     |
161 | 159, 160 | mpbi 213 |
. . . . . . . . . . . . . . . . 17
                         |
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . 16
                 


     
                          |
163 | 154, 155,
162 | rabfodom 28219 |
. . . . . . . . . . . . . . 15
                 


     
                            |
164 | | sneq 3969 |
. . . . . . . . . . . . . . . . . . . 20
       |
165 | 164 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . . . 19
                 |
166 | 165 | unieqd 4200 |
. . . . . . . . . . . . . . . . . 18
                   |
167 | 166 | ineq1d 3624 |
. . . . . . . . . . . . . . . . 17
                       |
168 | 167 | neeq1d 2702 |
. . . . . . . . . . . . . . . 16
           
             |
169 | 168 | cbvrabv 3030 |
. . . . . . . . . . . . . . 15
            
            |
170 | 163, 169 | syl6breq 4435 |
. . . . . . . . . . . . . 14
                 


     
                       
    |
171 | 123 | rabex 4550 |
. . . . . . . . . . . . . . 15
 


        |
172 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . 21
                 


  |
173 | | nfrab1 2957 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
174 | 173 | nfel1 2626 |
. . . . . . . . . . . . . . . . . . . . 21
       |
175 | 172, 174 | nfan 2031 |
. . . . . . . . . . . . . . . . . . . 20
                  
         |
176 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . 20
  |
177 | 175, 176 | nfan 2031 |
. . . . . . . . . . . . . . . . . . 19
                   
       
  |
178 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . 19
             |
179 | 177, 178 | nfan 2031 |
. . . . . . . . . . . . . . . . . 18
         
     
            
         
   |
180 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . 19
       |
181 | 173, 180 | nfrex 2848 |
. . . . . . . . . . . . . . . . . 18
            |
182 | 39 | ad5antlr 749 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
     
          |
183 | 182 | ad5antr 748 |
. . . . . . . . . . . . . . . . . . . . . 22
                     


     
         
            
  |
184 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . 22
                     


     
         
            
         |
185 | | fniniseg 6018 |
. . . . . . . . . . . . . . . . . . . . . . 23
        

        |
186 | 185 | biimpa 492 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                |
187 | 183, 184,
186 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
                     


     
         
            
        |
188 | 187 | simpld 466 |
. . . . . . . . . . . . . . . . . . . 20
                     


     
         
            
  |
189 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
                     


     
         
            
    |
190 | | rabid 2953 |
. . . . . . . . . . . . . . . . . . . 20
           |
191 | 188, 189,
190 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . 19
                     


     
         
            
      |
192 | 187 | simprd 470 |
. . . . . . . . . . . . . . . . . . 19
                     


     
         
            
      |
193 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
194 | 193 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
195 | 194 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . 19
                      |
196 | 191, 192,
195 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
                     


     
         
            
           |
197 | | uniinn0 28241 |
. . . . . . . . . . . . . . . . . . . 20
         
              |
198 | 197 | biimpi 199 |
. . . . . . . . . . . . . . . . . . 19
         

             |
199 | 198 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
                   
       
         
               |
200 | 179, 181,
196, 199 | r19.29af2 2915 |
. . . . . . . . . . . . . . . . 17
                   
       
         
             |
201 | 200 | ex 441 |
. . . . . . . . . . . . . . . 16
                  
       
                        |
202 | 201 | ss2rabdv 3496 |
. . . . . . . . . . . . . . 15
                 


     
         
   


         |
203 | | ssdomg 7633 |
. . . . . . . . . . . . . . 15
                      
   


                
   


          |
204 | 171, 202,
203 | mpsyl 64 |
. . . . . . . . . . . . . 14
                 


     
         
   


         |
205 | | domtr 7640 |
. . . . . . . . . . . . . 14
   
                     
               


        

             


         |
206 | 170, 204,
205 | syl2anc 673 |
. . . . . . . . . . . . 13
                 


     
               


         |
207 | 182 | adantr 472 |
. . . . . . . . . . . . . 14
                 


     
  |
208 | | dffn3 5748 |
. . . . . . . . . . . . . . 15

      |
209 | 208 | biimpi 199 |
. . . . . . . . . . . . . 14
    
  |
210 | | ssrab2 3500 |
. . . . . . . . . . . . . . 15
     |
211 | | fimarab 28320 |
. . . . . . . . . . . . . . 15
                   
            |
212 | 210, 211 | mpan2 685 |
. . . . . . . . . . . . . 14
              


         |
213 | 207, 209,
212 | 3syl 18 |
. . . . . . . . . . . . 13
                 


     
                     |
214 | 206, 213 | breqtrrd 4422 |
. . . . . . . . . . . 12
                 


     
                        |
215 | | domfi 7811 |
. . . . . . . . . . . 12
                                 

              |
216 | 141, 214,
215 | syl2anc 673 |
. . . . . . . . . . 11
                 


     
                |
217 | 216 | ex 441 |
. . . . . . . . . 10
     
     
                              |
218 | 217 | imdistanda 707 |
. . . . . . . . 9
               
                            |
219 | 218 | imp 436 |
. . . . . . . 8
     
     
                                |
220 | | simplll 776 |
. . . . . . . . 9
              
   |
221 | | locfinref.x |
. . . . . . . . . . . . 13
  |
222 | 221, 29 | islocfin 20609 |
. . . . . . . . . . . 12
     




        |
223 | 2, 222 | sylib 201 |
. . . . . . . . . . 11
    

        |
224 | 223 | simp3d 1044 |
. . . . . . . . . 10
  

       |
225 | 224 | r19.21bi 2776 |
. . . . . . . . 9
 
 

       |
226 | 220, 225 | sylancom 680 |
. . . . . . . 8
              
 

       |
227 | 136, 137,
219, 226 | reximd2a 2854 |
. . . . . . 7
              
 

                 |
228 | 227 | ralrimiva 2809 |
. . . . . 6
              


 
               |
229 | 221, 127 | islocfin 20609 |
. . . . . 6
              
 
                               |
230 | 131, 134,
228, 229 | syl3anbrc 1214 |
. . . . 5
                              |
231 | | funeq 5608 |
. . . . . . . 8
                         |
232 | | dmeq 5040 |
. . . . . . . . 9
          
            |
233 | 232 | sseq1d 3445 |
. . . . . . . 8
                         |
234 | | rneq 5066 |
. . . . . . . . 9
          
            |
235 | 234 | sseq1d 3445 |
. . . . . . . 8
                         |
236 | 231, 233,
235 | 3anbi123d 1365 |
. . . . . . 7
             
 
         
                       |
237 | 234 | breq1d 4405 |
. . . . . . . 8
                             |
238 | 234 | eleq1d 2533 |
. . . . . . . 8
                                 |
239 | 237, 238 | anbi12d 725 |
. . . . . . 7
              
     
            
                 |
240 | 236, 239 | anbi12d 725 |
. . . . . 6
                                    
                                 
                  |
241 | 124, 240 | spcev 3127 |
. . . . 5
                                               
              
    
  
        |
242 | 8, 13, 28, 130, 230, 241 | syl32anc 1300 |
. . . 4
                     
        |
243 | 242 | expl 630 |
. . 3
       
         
  
         |
244 | 243 | exlimdv 1787 |
. 2
                      
         |
245 | 6, 244 | mpd 15 |
1
                 |