Step | Hyp | Ref
| Expression |
1 | | vex 3048 |
. . . . . . . 8
 |
2 | | vex 3048 |
. . . . . . . 8
 |
3 | 1, 2 | xpex 6595 |
. . . . . . 7
   |
4 | 3 | rgen2w 2750 |
. . . . . 6


   |
5 | | eqid 2451 |
. . . . . . 7
           |
6 | | eleq2 2518 |
. . . . . . . 8
               |
7 | | sseq2 3454 |
. . . . . . . . 9
       
         |
8 | 7 | rexbidv 2901 |
. . . . . . . 8
    
   

         |
9 | 6, 8 | imbi12d 322 |
. . . . . . 7
        
           
          |
10 | 5, 9 | ralrnmpt2 6411 |
. . . . . 6
 

   


      


      
      
          |
11 | 4, 10 | ax-mp 5 |
. . . . 5
 
          
      
      
         |
12 | | opelxp 4864 |
. . . . . . . . . . . . . . . 16
  
       |
13 | | ancom 452 |
. . . . . . . . . . . . . . . 16
 
 
   |
14 | 12, 13 | bitri 253 |
. . . . . . . . . . . . . . 15
  
       |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
      

    |
16 | | r19.40 2941 |
. . . . . . . . . . . . . . . . 17
        
      

    

       |
17 | | raleq 2987 |
. . . . . . . . . . . . . . . . . . 19
  
   

       |
18 | 17 | cbvrexv 3020 |
. . . . . . . . . . . . . . . . . 18
  
   
 
      |
19 | | raleq 2987 |
. . . . . . . . . . . . . . . . . . 19
  
   

       |
20 | 19 | cbvrexv 3020 |
. . . . . . . . . . . . . . . . . 18
  
   
 
      |
21 | 18, 20 | anbi12i 703 |
. . . . . . . . . . . . . . . . 17
   
    

    
 

   


       |
22 | 16, 21 | sylib 200 |
. . . . . . . . . . . . . . . 16
        
      

     
       |
23 | | reeanv 2958 |
. . . . . . . . . . . . . . . . 17
  
 
         
 

   


       |
24 | | txflf.l |
. . . . . . . . . . . . . . . . . . . . 21
       |
25 | | filin 20869 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 
   |
26 | 25 | 3expb 1209 |
. . . . . . . . . . . . . . . . . . . . 21
      
 
    |
27 | 24, 26 | sylan 474 |
. . . . . . . . . . . . . . . . . . . 20
 

      |
28 | | inss1 3652 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
29 | | ssralv 3493 |
. . . . . . . . . . . . . . . . . . . . . 22
    
    

         |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
          |
31 | | inss2 3653 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
32 | | ssralv 3493 |
. . . . . . . . . . . . . . . . . . . . . 22
    
    

         |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
          |
34 | 30, 33 | anim12i 570 |
. . . . . . . . . . . . . . . . . . . 20
                                 |
35 | | raleq 2987 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   
           |
36 | | raleq 2987 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   
           |
37 | 35, 36 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . 21
               
 
                   |
38 | 37 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . . 20
                              
       |
39 | 27, 34, 38 | syl2an 480 |
. . . . . . . . . . . . . . . . . . 19
   
 
 
   

      
 
   

       |
40 | 39 | ex 436 |
. . . . . . . . . . . . . . . . . 18
 

    
                 
        |
41 | 40 | rexlimdvva 2886 |
. . . . . . . . . . . . . . . . 17
     
                 
        |
42 | 23, 41 | syl5bir 222 |
. . . . . . . . . . . . . . . 16
   

     
            
        |
43 | 22, 42 | impbid2 208 |
. . . . . . . . . . . . . . 15
    
         
 

   


        |
44 | | df-ima 4847 |
. . . . . . . . . . . . . . . . . . 19
       |
45 | | filelss 20867 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
46 | 24, 45 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
47 | | txflf.h |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
48 | 47 | reseq1i 5101 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
49 | | resmpt 5154 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
50 | 48, 49 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
51 | 46, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
                  |
52 | 51 | rneqd 5062 |
. . . . . . . . . . . . . . . . . . 19
 
 
                |
53 | 44, 52 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . 18
 
                    |
54 | 53 | sseq1d 3459 |
. . . . . . . . . . . . . . . . 17
 
     
 
                  |
55 | | opelxp 4864 |
. . . . . . . . . . . . . . . . . . 19
                          |
56 | 55 | ralbii 2819 |
. . . . . . . . . . . . . . . . . 18
 
             
            |
57 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . 20
                           |
58 | 57 | fmpt 6043 |
. . . . . . . . . . . . . . . . . . 19
 
                                  |
59 | | opex 4664 |
. . . . . . . . . . . . . . . . . . . . 21
            |
60 | 59, 57 | fnmpti 5706 |
. . . . . . . . . . . . . . . . . . . 20
              |
61 | | df-f 5586 |
. . . . . . . . . . . . . . . . . . . 20
                   
                          
     |
62 | 60, 61 | mpbiran 929 |
. . . . . . . . . . . . . . . . . . 19
                   
                 |
63 | 58, 62 | bitri 253 |
. . . . . . . . . . . . . . . . . 18
 
                         
    |
64 | | r19.26 2917 |
. . . . . . . . . . . . . . . . . 18
 
         
 
   

       |
65 | 56, 63, 64 | 3bitr3i 279 |
. . . . . . . . . . . . . . . . 17
             
 
 
   

       |
66 | 54, 65 | syl6bb 265 |
. . . . . . . . . . . . . . . 16
 
     
 
 
   

        |
67 | 66 | rexbidva 2898 |
. . . . . . . . . . . . . . 15
         
      
        |
68 | | txflf.f |
. . . . . . . . . . . . . . . . . . . 20
       |
69 | 68 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
       |
70 | | ffun 5731 |
. . . . . . . . . . . . . . . . . . 19
       |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
   |
72 | | filelss 20867 |
. . . . . . . . . . . . . . . . . . . 20
         |
73 | 24, 72 | sylan 474 |
. . . . . . . . . . . . . . . . . . 19
 
   |
74 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . 20
       |
75 | 69, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
   |
76 | 73, 75 | sseqtr4d 3469 |
. . . . . . . . . . . . . . . . . 18
 
   |
77 | | funimass4 5916 |
. . . . . . . . . . . . . . . . . 18
                |
78 | 71, 76, 77 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
     

       |
79 | 78 | rexbidva 2898 |
. . . . . . . . . . . . . . . 16
        
       |
80 | | txflf.g |
. . . . . . . . . . . . . . . . . . . 20
       |
81 | 80 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
       |
82 | | ffun 5731 |
. . . . . . . . . . . . . . . . . . 19
       |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
   |
84 | | filelss 20867 |
. . . . . . . . . . . . . . . . . . . 20
         |
85 | 24, 84 | sylan 474 |
. . . . . . . . . . . . . . . . . . 19
 
   |
86 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . 20
       |
87 | 81, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
   |
88 | 85, 87 | sseqtr4d 3469 |
. . . . . . . . . . . . . . . . . 18
 
   |
89 | | funimass4 5916 |
. . . . . . . . . . . . . . . . . 18
                |
90 | 83, 88, 89 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
     

       |
91 | 90 | rexbidva 2898 |
. . . . . . . . . . . . . . . 16
        
       |
92 | 79, 91 | anbi12d 717 |
. . . . . . . . . . . . . . 15
   
         
 

   


        |
93 | 43, 67, 92 | 3bitr4d 289 |
. . . . . . . . . . . . . 14
                        |
94 | 15, 93 | imbi12d 322 |
. . . . . . . . . . . . 13
        
      
 
                 |
95 | | impexp 448 |
. . . . . . . . . . . . 13
   
 
          

  
    
         |
96 | 94, 95 | syl6bb 265 |
. . . . . . . . . . . 12
        
      

  
    
          |
97 | 96 | ralbidv 2827 |
. . . . . . . . . . 11
         
      


  
    
          |
98 | | eleq2 2518 |
. . . . . . . . . . . . 13
 
   |
99 | 98 | ralrab 3200 |
. . . . . . . . . . . 12
 

   
    
     


  
    
         |
100 | | r19.21v 2793 |
. . . . . . . . . . . 12
 

   
    
     

 
  
             |
101 | 99, 100 | bitr3i 255 |
. . . . . . . . . . 11
 

               
 
  
             |
102 | 97, 101 | syl6bb 265 |
. . . . . . . . . 10
         
      

 
  
              |
103 | 102 | ralbidv 2827 |
. . . . . . . . 9
          
      


 
  
              |
104 | | eleq2 2518 |
. . . . . . . . . 10
 
   |
105 | 104 | ralrab 3200 |
. . . . . . . . 9
 

   
  
         


 
  
             |
106 | 103, 105 | syl6bbr 267 |
. . . . . . . 8
          
      
 
   
                |
107 | 106 | adantr 467 |
. . . . . . 7
 

           
      
 
   
                |
108 | | txflf.j |
. . . . . . . . . . 11
 TopOn    |
109 | | toponmax 19943 |
. . . . . . . . . . 11
 TopOn 
  |
110 | 108, 109 | syl 17 |
. . . . . . . . . 10
   |
111 | | eleq2 2518 |
. . . . . . . . . . . 12
 
   |
112 | 111 | rspcev 3150 |
. . . . . . . . . . 11
 
 
  |
113 | | rabn0 3752 |
. . . . . . . . . . 11
 
 
  |
114 | 112, 113 | sylibr 216 |
. . . . . . . . . 10
 
 
   |
115 | 110, 114 | sylan 474 |
. . . . . . . . 9
 
 
   |
116 | | txflf.k |
. . . . . . . . . . 11
 TopOn    |
117 | | toponmax 19943 |
. . . . . . . . . . 11
 TopOn 
  |
118 | 116, 117 | syl 17 |
. . . . . . . . . 10
   |
119 | | eleq2 2518 |
. . . . . . . . . . . 12
 
   |
120 | 119 | rspcev 3150 |
. . . . . . . . . . 11
 
 
  |
121 | | rabn0 3752 |
. . . . . . . . . . 11
 
 
  |
122 | 120, 121 | sylibr 216 |
. . . . . . . . . 10
 
 
   |
123 | 118, 122 | sylan 474 |
. . . . . . . . 9
 
 
   |
124 | 115, 123 | anim12dan 848 |
. . . . . . . 8
 

     
    |
125 | | r19.28zv 3864 |
. . . . . . . . . 10
 

 

       
    
 
     
           |
126 | 125 | ralbidv 2827 |
. . . . . . . . 9
 

 

   
  
         
 
  
     
  
        |
127 | | r19.27zv 3869 |
. . . . . . . . 9
 

 

       

  
       
       

  
        |
128 | 126, 127 | sylan9bbr 707 |
. . . . . . . 8
  
 
    
   
            
 

  
     
  
        |
129 | 124, 128 | syl 17 |
. . . . . . 7
 

    
   
            
 

  
     
  
        |
130 | 107, 129 | bitrd 257 |
. . . . . 6
 

           
      
 

  
     
  
        |
131 | 104 | ralrab 3200 |
. . . . . . 7
 

  
      
       |
132 | 98 | ralrab 3200 |
. . . . . . 7
 

  
      
       |
133 | 131, 132 | anbi12i 703 |
. . . . . 6
   
  
    

  
      


    



        |
134 | 130, 133 | syl6bb 265 |
. . . . 5
 

           
      
 

        
         |
135 | 11, 134 | syl5bb 261 |
. . . 4
 

             

      


    



         |
136 | 135 | pm5.32da 647 |
. . 3
     
          
     
 
   

    



          |
137 | | opelxp 4864 |
. . . 4
  
       |
138 | 137 | anbi1i 701 |
. . 3
      
          

     
 
  

      


        |
139 | | an4 833 |
. . 3
    
        


      
 
   

    



         |
140 | 136, 138,
139 | 3bitr4g 292 |
. 2
                   
        


      
  
          |
141 | | eqid 2451 |
. . . . . . . 8
           |
142 | 141 | txval 20579 |
. . . . . . 7
  TopOn  TopOn  
             |
143 | 108, 116,
142 | syl2anc 667 |
. . . . . 6
              |
144 | 143 | oveq1d 6305 |
. . . . 5
                  |
145 | 144 | fveq1d 5867 |
. . . 4
                   
      |
146 | 145 | eleq2d 2514 |
. . 3
                          
       |
147 | | txtopon 20606 |
. . . . . 6
  TopOn  TopOn  
  TopOn      |
148 | 108, 116,
147 | syl2anc 667 |
. . . . 5
   TopOn 
    |
149 | 143, 148 | eqeltrrd 2530 |
. . . 4
          TopOn 
    |
150 | 68 | ffvelrnda 6022 |
. . . . . 6
 
       |
151 | 80 | ffvelrnda 6022 |
. . . . . 6
 
       |
152 | | opelxpi 4866 |
. . . . . 6
                          |
153 | 150, 151,
152 | syl2anc 667 |
. . . . 5
 
                |
154 | 153, 47 | fmptd 6046 |
. . . 4
         |
155 | | eqid 2451 |
. . . . 5
            

     |
156 | 155 | flftg 21011 |
. . . 4
           TopOn 
     
                                           
         |
157 | 149, 24, 154, 156 | syl3anc 1268 |
. . 3
               
   
                

         |
158 | 146, 157 | bitrd 257 |
. 2
                              
         |
159 | | isflf 21008 |
. . . 4
  TopOn     
     
     




         |
160 | 108, 24, 68, 159 | syl3anc 1268 |
. . 3
       




         |
161 | | isflf 21008 |
. . . 4
  TopOn     
     
     




         |
162 | 116, 24, 80, 161 | syl3anc 1268 |
. . 3
       




         |
163 | 160, 162 | anbi12d 717 |
. 2
                  


      
  
          |
164 | 140, 158,
163 | 3bitr4d 289 |
1
                              |