Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . 4
   TopOn   
        TopOn    |
2 | | toptopon2 13759 |
. . . . . 6

TopOn     |
3 | 2 | biimpi 120 |
. . . . 5
 TopOn     |
4 | 3 | ad2antlr 489 |
. . . 4
   TopOn   
        TopOn     |
5 | | simpr3 1006 |
. . . 4
   TopOn   
                |
6 | | cnpf2 13947 |
. . . 4
  TopOn  TopOn         
       |
7 | 1, 4, 5, 6 | syl3anc 1248 |
. . 3
   TopOn   
               |
8 | | simpr1 1004 |
. . 3
   TopOn   
          |
9 | 7, 8 | fssresd 5404 |
. 2
   TopOn   
                 |
10 | | simplr2 1041 |
. . . . . 6
    TopOn 
 
           |
11 | | fvres 5551 |
. . . . . 6
             |
12 | 10, 11 | syl 14 |
. . . . 5
    TopOn 
 
                     |
13 | 12 | eleq1d 2256 |
. . . 4
    TopOn 
 
               
       |
14 | 1 | ad2antrr 488 |
. . . . . . 7
     TopOn 


              TopOn    |
15 | 4 | ad2antrr 488 |
. . . . . . 7
     TopOn 


              TopOn     |
16 | 8 | ad2antrr 488 |
. . . . . . . 8
     TopOn 


                |
17 | | simpr2 1005 |
. . . . . . . . 9
   TopOn   
          |
18 | 17 | ad2antrr 488 |
. . . . . . . 8
     TopOn 


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


                |
20 | 5 | ad2antrr 488 |
. . . . . . 7
     TopOn 


                      |
21 | | simplr 528 |
. . . . . . 7
     TopOn 


                |
22 | | simpr 110 |
. . . . . . 7
     TopOn 


                    |
23 | | icnpimaex 13951 |
. . . . . . 7
   TopOn  TopOn   
            


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


              

       |
25 | 24 | ex 115 |
. . . . 5
    TopOn 
 
              

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

    |
28 | | elin 3330 |
. . . . . . . . . 10
  

   |
29 | 27, 28 | imbitrrdi 162 |
. . . . . . . . 9
   TopOn   
        
     |
30 | | inss1 3367 |
. . . . . . . . . . . 12
   |
31 | | imass2 5016 |
. . . . . . . . . . . 12
               |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . 11
           |
33 | | id 19 |
. . . . . . . . . . 11
           |
34 | 32, 33 | sstrid 3178 |
. . . . . . . . . 10
             |
35 | 34 | a1i 9 |
. . . . . . . . 9
   TopOn   
            
         |
36 | 29, 35 | anim12d 335 |
. . . . . . . 8
   TopOn   
             
              |
37 | 36 | reximdv 2588 |
. . . . . . 7
   TopOn   
         

   
  

    
 
    |
38 | | vex 2752 |
. . . . . . . . . 10
 |
39 | 38 | inex1 4149 |
. . . . . . . . 9
   |
40 | 39 | a1i 9 |
. . . . . . . 8
    TopOn 
 
         
   |
41 | | topontop 13754 |
. . . . . . . . . 10
 TopOn 
  |
42 | 41 | ad2antrr 488 |
. . . . . . . . 9
   TopOn   
          |
43 | | uniexg 4451 |
. . . . . . . . . . 11
    |
44 | 42, 43 | syl 14 |
. . . . . . . . . 10
   TopOn   
           |
45 | | toponuni 13755 |
. . . . . . . . . . . . 13
 TopOn 
   |
46 | 45 | sseq2d 3197 |
. . . . . . . . . . . 12
 TopOn 

    |
47 | 46 | ad2antrr 488 |
. . . . . . . . . . 11
   TopOn   
        
    |
48 | 8, 47 | mpbid 147 |
. . . . . . . . . 10
   TopOn   
           |
49 | 44, 48 | ssexd 4155 |
. . . . . . . . 9
   TopOn   
          |
50 | | elrest 12712 |
. . . . . . . . 9
 
   ↾t 


    |
51 | 42, 49, 50 | syl2anc 411 |
. . . . . . . 8
   TopOn   
          ↾t  
     |
52 | | simpr 110 |
. . . . . . . . . 10
    TopOn 
 
               |
53 | 52 | eleq2d 2257 |
. . . . . . . . 9
    TopOn 
 
                 |
54 | 52 | imaeq2d 4982 |
. . . . . . . . . . 11
    TopOn 
 
                  
        |
55 | | inss2 3368 |
. . . . . . . . . . . 12
   |
56 | | resima2 4953 |
. . . . . . . . . . . 12
              
    |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . 11
 
         
   |
58 | 54, 57 | eqtrdi 2236 |
. . . . . . . . . 10
    TopOn 
 
                         |
59 | 58 | sseq1d 3196 |
. . . . . . . . 9
    TopOn 
 
                 
         |
60 | 53, 59 | anbi12d 473 |
. . . . . . . 8
    TopOn 
 
              
    
  
          |
61 | 40, 51, 60 | rexxfr2d 4477 |
. . . . . . 7
   TopOn   
         
 ↾t          

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

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

   
   ↾t              |
64 | 25, 63 | syld 45 |
. . . 4
    TopOn 
 
              
 ↾t              |
65 | 13, 64 | sylbid 150 |
. . 3
    TopOn 
 
                
 ↾t              |
66 | 65 | ralrimiva 2560 |
. 2
   TopOn   
        
      
 
↾t              |
67 | | resttopon 13911 |
. . . 4
  TopOn    ↾t  TopOn    |
68 | 1, 8, 67 | syl2anc 411 |
. . 3
   TopOn   
         ↾t  TopOn    |
69 | | iscnp 13939 |
. . 3
  
↾t  TopOn  TopOn   
      ↾t     
        
       
 ↾t                |
70 | 68, 4, 17, 69 | syl3anc 1248 |
. 2
   TopOn   
              ↾t                      
 ↾t                |
71 | 9, 66, 70 | mpbir2and 945 |
1
   TopOn   
             ↾t        |