Step | Hyp | Ref
| Expression |
1 | | simpll 501 |
. . . 4
   TopOn   
        TopOn    |
2 | | toptopon2 12029 |
. . . . . 6

TopOn     |
3 | 2 | biimpi 119 |
. . . . 5
 TopOn     |
4 | 3 | ad2antlr 478 |
. . . 4
   TopOn   
        TopOn     |
5 | | simpr3 972 |
. . . 4
   TopOn   
                |
6 | | cnpf2 12218 |
. . . 4
  TopOn  TopOn         
       |
7 | 1, 4, 5, 6 | syl3anc 1199 |
. . 3
   TopOn   
               |
8 | | simpr1 970 |
. . 3
   TopOn   
          |
9 | 7, 8 | fssresd 5257 |
. 2
   TopOn   
                 |
10 | | simplr2 1007 |
. . . . . 6
    TopOn 
 
           |
11 | | fvres 5399 |
. . . . . 6
             |
12 | 10, 11 | syl 14 |
. . . . 5
    TopOn 
 
                     |
13 | 12 | eleq1d 2183 |
. . . 4
    TopOn 
 
               
       |
14 | 1 | ad2antrr 477 |
. . . . . . 7
     TopOn 


              TopOn    |
15 | 4 | ad2antrr 477 |
. . . . . . 7
     TopOn 


              TopOn     |
16 | 8 | ad2antrr 477 |
. . . . . . . 8
     TopOn 


                |
17 | | simpr2 971 |
. . . . . . . . 9
   TopOn   
          |
18 | 17 | ad2antrr 477 |
. . . . . . . 8
     TopOn 


                |
19 | 16, 18 | sseldd 3064 |
. . . . . . 7
     TopOn 


                |
20 | 5 | ad2antrr 477 |
. . . . . . 7
     TopOn 


                      |
21 | | simplr 502 |
. . . . . . 7
     TopOn 


                |
22 | | simpr 109 |
. . . . . . 7
     TopOn 


                    |
23 | | icnpimaex 12222 |
. . . . . . 7
   TopOn  TopOn   
            


       |
24 | 14, 15, 19, 20, 21, 22, 23 | syl33anc 1214 |
. . . . . 6
     TopOn 


              

       |
25 | 24 | ex 114 |
. . . . 5
    TopOn 
 
              

   
    |
26 | | idd 21 |
. . . . . . . . . . 11
   TopOn   
        
   |
27 | 26, 17 | jctird 313 |
. . . . . . . . . 10
   TopOn   
        

    |
28 | | elin 3225 |
. . . . . . . . . 10
  

   |
29 | 27, 28 | syl6ibr 161 |
. . . . . . . . 9
   TopOn   
        
     |
30 | | inss1 3262 |
. . . . . . . . . . . 12
   |
31 | | imass2 4873 |
. . . . . . . . . . . 12
               |
32 | 30, 31 | ax-mp 7 |
. . . . . . . . . . 11
           |
33 | | id 19 |
. . . . . . . . . . 11
           |
34 | 32, 33 | sstrid 3074 |
. . . . . . . . . 10
             |
35 | 34 | a1i 9 |
. . . . . . . . 9
   TopOn   
            
         |
36 | 29, 35 | anim12d 331 |
. . . . . . . 8
   TopOn   
             
              |
37 | 36 | reximdv 2507 |
. . . . . . 7
   TopOn   
         

   
  

    
 
    |
38 | | vex 2660 |
. . . . . . . . . 10
 |
39 | 38 | inex1 4022 |
. . . . . . . . 9
   |
40 | 39 | a1i 9 |
. . . . . . . 8
    TopOn 
 
         
   |
41 | | topontop 12024 |
. . . . . . . . . 10
 TopOn 
  |
42 | 41 | ad2antrr 477 |
. . . . . . . . 9
   TopOn   
          |
43 | | uniexg 4321 |
. . . . . . . . . . 11
    |
44 | 42, 43 | syl 14 |
. . . . . . . . . 10
   TopOn   
           |
45 | | toponuni 12025 |
. . . . . . . . . . . . 13
 TopOn 
   |
46 | 45 | sseq2d 3093 |
. . . . . . . . . . . 12
 TopOn 

    |
47 | 46 | ad2antrr 477 |
. . . . . . . . . . 11
   TopOn   
        
    |
48 | 8, 47 | mpbid 146 |
. . . . . . . . . 10
   TopOn   
           |
49 | 44, 48 | ssexd 4028 |
. . . . . . . . 9
   TopOn   
          |
50 | | elrest 11970 |
. . . . . . . . 9
 
   ↾t 


    |
51 | 42, 49, 50 | syl2anc 406 |
. . . . . . . 8
   TopOn   
          ↾t  
     |
52 | | simpr 109 |
. . . . . . . . . 10
    TopOn 
 
               |
53 | 52 | eleq2d 2184 |
. . . . . . . . 9
    TopOn 
 
                 |
54 | 52 | imaeq2d 4839 |
. . . . . . . . . . 11
    TopOn 
 
                  
        |
55 | | inss2 3263 |
. . . . . . . . . . . 12
   |
56 | | resima2 4811 |
. . . . . . . . . . . 12
              
    |
57 | 55, 56 | ax-mp 7 |
. . . . . . . . . . 11
 
         
   |
58 | 54, 57 | syl6eq 2163 |
. . . . . . . . . 10
    TopOn 
 
                         |
59 | 58 | sseq1d 3092 |
. . . . . . . . 9
    TopOn 
 
                 
         |
60 | 53, 59 | anbi12d 462 |
. . . . . . . 8
    TopOn 
 
              
    
  
          |
61 | 40, 51, 60 | rexxfr2d 4346 |
. . . . . . 7
   TopOn   
         
 ↾t          

  
          |
62 | 37, 61 | sylibrd 168 |
. . . . . 6
   TopOn   
         

   
   ↾t              |
63 | 62 | adantr 272 |
. . . . 5
    TopOn 
 
          

   
   ↾t              |
64 | 25, 63 | syld 45 |
. . . 4
    TopOn 
 
              
 ↾t              |
65 | 13, 64 | sylbid 149 |
. . 3
    TopOn 
 
                
 ↾t              |
66 | 65 | ralrimiva 2479 |
. 2
   TopOn   
        
      
 
↾t              |
67 | | resttopon 12183 |
. . . 4
  TopOn    ↾t  TopOn    |
68 | 1, 8, 67 | syl2anc 406 |
. . 3
   TopOn   
         ↾t  TopOn    |
69 | | iscnp 12210 |
. . 3
  
↾t  TopOn  TopOn   
      ↾t     
        
       
 ↾t                |
70 | 68, 4, 17, 69 | syl3anc 1199 |
. 2
   TopOn   
              ↾t                      
 ↾t                |
71 | 9, 66, 70 | mpbir2and 911 |
1
   TopOn   
             ↾t        |