Step | Hyp | Ref
| Expression |
1 | | cntop1 13368 |
. . . 4
     |
2 | 1 | a1i 9 |
. . 3
  TopOn   
     |
3 | | eqid 2177 |
. . . . . . . 8
   |
4 | | eqid 2177 |
. . . . . . . 8
   |
5 | 3, 4 | cnf 13371 |
. . . . . . 7
           |
6 | 5 | ffnd 5362 |
. . . . . 6
      |
7 | 6 | a1i 9 |
. . . . 5
  TopOn   
      |
8 | | simp2 998 |
. . . . 5
  TopOn     |
9 | 7, 8 | jctird 317 |
. . . 4
  TopOn   
  

    |
10 | | df-f 5216 |
. . . 4
     
     |
11 | 9, 10 | syl6ibr 162 |
. . 3
  TopOn   
          |
12 | 2, 11 | jcad 307 |
. 2
  TopOn   
  
         |
13 | | cntop1 13368 |
. . . . 5
  
↾t  
  |
14 | 13 | adantl 277 |
. . . 4
   TopOn     ↾t      |
15 | 3 | toptopon 13183 |
. . . . . 6

TopOn     |
16 | 14, 15 | sylib 122 |
. . . . 5
   TopOn     ↾t    TopOn     |
17 | | resttopon 13338 |
. . . . . . 7
  TopOn    ↾t  TopOn    |
18 | 17 | 3adant2 1016 |
. . . . . 6
  TopOn    ↾t  TopOn    |
19 | 18 | adantr 276 |
. . . . 5
   TopOn     ↾t     ↾t  TopOn    |
20 | | simpr 110 |
. . . . 5
   TopOn     ↾t      ↾t     |
21 | | cnf2 13372 |
. . . . 5
  TopOn    ↾t  TopOn    ↾t           |
22 | 16, 19, 20, 21 | syl3anc 1238 |
. . . 4
   TopOn     ↾t           |
23 | 14, 22 | jca 306 |
. . 3
   TopOn     ↾t    
        |
24 | 23 | ex 115 |
. 2
  TopOn   
 
↾t             |
25 | | vex 2740 |
. . . . . . . . 9
 |
26 | 25 | inex1 4134 |
. . . . . . . 8
   |
27 | 26 | a1i 9 |
. . . . . . 7
    TopOn 
 
       
    |
28 | | simpl1 1000 |
. . . . . . . 8
   TopOn   
      
TopOn    |
29 | | toponmax 13190 |
. . . . . . . . . 10
 TopOn 
  |
30 | 28, 29 | syl 14 |
. . . . . . . . 9
   TopOn   
      
  |
31 | | simpl3 1002 |
. . . . . . . . 9
   TopOn   
      
  |
32 | 30, 31 | ssexd 4140 |
. . . . . . . 8
   TopOn   
      
  |
33 | | elrest 12643 |
. . . . . . . 8
  TopOn     ↾t  
     |
34 | 28, 32, 33 | syl2anc 411 |
. . . . . . 7
   TopOn   
      
 
↾t 


    |
35 | | imaeq2 4962 |
. . . . . . . . 9
                 |
36 | 35 | eleq1d 2246 |
. . . . . . . 8
                   |
37 | 36 | adantl 277 |
. . . . . . 7
    TopOn 
 
         
     
          |
38 | 27, 34, 37 | ralxfr2d 4461 |
. . . . . 6
   TopOn   
      
 
 ↾t                   |
39 | | simplrr 536 |
. . . . . . . . . 10
    TopOn 
 
       
       |
40 | | ffun 5364 |
. . . . . . . . . 10
        |
41 | | inpreima 5638 |
. . . . . . . . . 10

                     |
42 | 39, 40, 41 | 3syl 17 |
. . . . . . . . 9
    TopOn 
 
       
                     |
43 | | cnvimass 4987 |
. . . . . . . . . . . 12
    
 |
44 | | cnvimarndm 4988 |
. . . . . . . . . . . 12
      |
45 | 43, 44 | sseqtrri 3190 |
. . . . . . . . . . 11
           |
46 | | simpll2 1037 |
. . . . . . . . . . . 12
    TopOn 
 
       
  |
47 | | imass2 5000 |
. . . . . . . . . . . 12

    
       |
48 | 46, 47 | syl 14 |
. . . . . . . . . . 11
    TopOn 
 
       
            |
49 | 45, 48 | sstrid 3166 |
. . . . . . . . . 10
    TopOn 
 
       
            |
50 | | df-ss 3142 |
. . . . . . . . . 10
          
                   |
51 | 49, 50 | sylib 122 |
. . . . . . . . 9
    TopOn 
 
       
                   |
52 | 42, 51 | eqtrd 2210 |
. . . . . . . 8
    TopOn 
 
       
              |
53 | 52 | eleq1d 2246 |
. . . . . . 7
    TopOn 
 
       
       
        |
54 | 53 | ralbidva 2473 |
. . . . . 6
   TopOn   
      
 
      

        |
55 | | simprr 531 |
. . . . . . . 8
   TopOn   
      
       |
56 | 55, 31 | fssd 5374 |
. . . . . . 7
   TopOn   
      
       |
57 | 56 | biantrurd 305 |
. . . . . 6
   TopOn   
      
 
    
                |
58 | 38, 54, 57 | 3bitrrd 215 |
. . . . 5
   TopOn   
      
             
 
↾t           |
59 | 55 | biantrurd 305 |
. . . . 5
   TopOn   
      
 
 ↾t               
↾t            |
60 | 58, 59 | bitrd 188 |
. . . 4
   TopOn   
      
             
        ↾t            |
61 | | simprl 529 |
. . . . . 6
   TopOn   
      
  |
62 | 61, 15 | sylib 122 |
. . . . 5
   TopOn   
      
TopOn     |
63 | | iscn 13364 |
. . . . 5
  TopOn   TopOn  
         
         |
64 | 62, 28, 63 | syl2anc 411 |
. . . 4
   TopOn   
      
         
         |
65 | 18 | adantr 276 |
. . . . 5
   TopOn   
      
 ↾t  TopOn    |
66 | | iscn 13364 |
. . . . 5
  TopOn    ↾t  TopOn      ↾t  
        ↾t            |
67 | 62, 65, 66 | syl2anc 411 |
. . . 4
   TopOn   
      
   ↾t  
        ↾t            |
68 | 60, 64, 67 | 3bitr4d 220 |
. . 3
   TopOn   
      
  
  ↾t      |
69 | 68 | ex 115 |
. 2
  TopOn           
 

 ↾t       |
70 | 12, 24, 69 | pm5.21ndd 705 |
1
  TopOn   
 

 ↾t      |