Step | Hyp | Ref
| Expression |
1 | | cnconst2 20299 |
. . . 4
  TopOn  TopOn 

        |
2 | 1 | 3expa 1208 |
. . 3
   TopOn  TopOn  
         |
3 | | eqid 2451 |
. . 3
             |
4 | 2, 3 | fmptd 6046 |
. 2
  TopOn  TopOn  

         
   |
5 | | eqid 2451 |
. . . . . 6
   |
6 | | eqid 2451 |
. . . . . 6
    ↾t     
 ↾t    |
7 | | eqid 2451 |
. . . . . 6
     ↾t                  ↾t              |
8 | 5, 6, 7 | xkobval 20601 |
. . . . 5
     ↾t                    ↾t             |
9 | 8 | abeq2i 2563 |
. . . 4
      ↾t            
   
 
↾t        
    |
10 | 2 | adantlr 721 |
. . . . . . . . . . . . . 14
    TopOn 
TopOn       
         |
11 | 10 | adantlr 721 |
. . . . . . . . . . . . 13
     TopOn 
TopOn        
↾t            |
12 | 11 | adantlr 721 |
. . . . . . . . . . . 12
      TopOn  TopOn  
  
 
 ↾t  

         |
13 | | simplr 762 |
. . . . . . . . . . . . . 14
      TopOn  TopOn  
  
 
 ↾t  

   |
14 | 13 | imaeq2d 5168 |
. . . . . . . . . . . . 13
      TopOn  TopOn  
  
 
 ↾t  

                   |
15 | | ima0 5183 |
. . . . . . . . . . . . . 14
         |
16 | | 0ss 3763 |
. . . . . . . . . . . . . 14
 |
17 | 15, 16 | eqsstri 3462 |
. . . . . . . . . . . . 13
         |
18 | 14, 17 | syl6eqss 3482 |
. . . . . . . . . . . 12
      TopOn  TopOn  
  
 
 ↾t  

           |
19 | | imaeq1 5163 |
. . . . . . . . . . . . . 14
                   |
20 | 19 | sseq1d 3459 |
. . . . . . . . . . . . 13
                     |
21 | 20 | elrab 3196 |
. . . . . . . . . . . 12
           
       
           |
22 | 12, 18, 21 | sylanbrc 670 |
. . . . . . . . . . 11
      TopOn  TopOn  
  
 
 ↾t  

               |
23 | 22 | ralrimiva 2802 |
. . . . . . . . . 10
     TopOn 
TopOn        
↾t    
              |
24 | | rabid2 2968 |
. . . . . . . . . 10
                          
   |
25 | 23, 24 | sylibr 216 |
. . . . . . . . 9
     TopOn 
TopOn        
↾t                    |
26 | | simpllr 769 |
. . . . . . . . . . 11
    TopOn 
TopOn        
↾t   TopOn    |
27 | | toponmax 19943 |
. . . . . . . . . . 11
 TopOn 
  |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
    TopOn 
TopOn        
↾t     |
29 | 28 | adantr 467 |
. . . . . . . . 9
     TopOn 
TopOn        
↾t      |
30 | 25, 29 | eqeltrrd 2530 |
. . . . . . . 8
     TopOn 
TopOn        
↾t    
               |
31 | | ifnefalse 3893 |
. . . . . . . . . . . . . . 15

       |
32 | 31 | ad2antlr 733 |
. . . . . . . . . . . . . 14
      TopOn  TopOn  
  
 
 ↾t  

        |
33 | 32 | eleq2d 2514 |
. . . . . . . . . . . . 13
      TopOn  TopOn  
  
 
 ↾t  

          |
34 | | vex 3048 |
. . . . . . . . . . . . . . . 16
 |
35 | 34 | snss 4096 |
. . . . . . . . . . . . . . 15

    |
36 | 33, 35 | syl6bb 265 |
. . . . . . . . . . . . . 14
      TopOn  TopOn  
  
 
 ↾t  

            |
37 | | df-ima 4847 |
. . . . . . . . . . . . . . . . 17
               |
38 | | simplrl 770 |
. . . . . . . . . . . . . . . . . . . . . 22
    TopOn 
TopOn        
↾t       |
39 | 38 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . 21
      TopOn  TopOn  
  
 
 ↾t  

     |
40 | 39 | elpwid 3961 |
. . . . . . . . . . . . . . . . . . . 20
      TopOn  TopOn  
  
 
 ↾t  


   |
41 | | toponuni 19942 |
. . . . . . . . . . . . . . . . . . . . 21
 TopOn 
   |
42 | 41 | ad5antr 740 |
. . . . . . . . . . . . . . . . . . . 20
      TopOn  TopOn  
  
 
 ↾t  

    |
43 | 40, 42 | sseqtr4d 3469 |
. . . . . . . . . . . . . . . . . . 19
      TopOn  TopOn  
  
 
 ↾t  


  |
44 | | xpssres 5139 |
. . . . . . . . . . . . . . . . . . 19
             |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      TopOn  TopOn  
  
 
 ↾t  

             |
46 | 45 | rneqd 5062 |
. . . . . . . . . . . . . . . . 17
      TopOn  TopOn  
  
 
 ↾t  

             |
47 | 37, 46 | syl5eq 2497 |
. . . . . . . . . . . . . . . 16
      TopOn  TopOn  
  
 
 ↾t  

               |
48 | | rnxp 5267 |
. . . . . . . . . . . . . . . . 17

        |
49 | 48 | ad2antlr 733 |
. . . . . . . . . . . . . . . 16
      TopOn  TopOn  
  
 
 ↾t  

         |
50 | 47, 49 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
      TopOn  TopOn  
  
 
 ↾t  

             |
51 | 50 | sseq1d 3459 |
. . . . . . . . . . . . . 14
      TopOn  TopOn  
  
 
 ↾t  

         
     |
52 | 11 | adantlr 721 |
. . . . . . . . . . . . . . 15
      TopOn  TopOn  
  
 
 ↾t  

         |
53 | 52 | biantrurd 511 |
. . . . . . . . . . . . . 14
      TopOn  TopOn  
  
 
 ↾t  

         
                   |
54 | 36, 51, 53 | 3bitr2d 285 |
. . . . . . . . . . . . 13
      TopOn  TopOn  
  
 
 ↾t  

                          |
55 | 33, 54 | bitr3d 259 |
. . . . . . . . . . . 12
      TopOn  TopOn  
  
 
 ↾t  

                     |
56 | 55, 21 | syl6bbr 267 |
. . . . . . . . . . 11
      TopOn  TopOn  
  
 
 ↾t  

                 |
57 | 56 | rabbi2dva 3640 |
. . . . . . . . . 10
     TopOn 
TopOn        
↾t                      |
58 | | simplrr 771 |
. . . . . . . . . . . . 13
    TopOn 
TopOn        
↾t     |
59 | | toponss 19944 |
. . . . . . . . . . . . 13
  TopOn     |
60 | 26, 58, 59 | syl2anc 667 |
. . . . . . . . . . . 12
    TopOn 
TopOn        
↾t     |
61 | 60 | adantr 467 |
. . . . . . . . . . 11
     TopOn 
TopOn        
↾t      |
62 | | dfss1 3637 |
. . . . . . . . . . 11

    |
63 | 61, 62 | sylib 200 |
. . . . . . . . . 10
     TopOn 
TopOn        
↾t        |
64 | 57, 63 | eqtr3d 2487 |
. . . . . . . . 9
     TopOn 
TopOn        
↾t    
               |
65 | 58 | adantr 467 |
. . . . . . . . 9
     TopOn 
TopOn        
↾t      |
66 | 64, 65 | eqeltrd 2529 |
. . . . . . . 8
     TopOn 
TopOn        
↾t    
               |
67 | 30, 66 | pm2.61dane 2711 |
. . . . . . 7
    TopOn 
TopOn        
↾t   
               |
68 | | imaeq2 5164 |
. . . . . . . . 9
        
                           
    |
69 | 3 | mptpreima 5328 |
. . . . . . . . 9
                                  |
70 | 68, 69 | syl6eq 2501 |
. . . . . . . 8
        
                           |
71 | 70 | eleq1d 2513 |
. . . . . . 7
        
           

                |
72 | 67, 71 | syl5ibrcom 226 |
. . . . . 6
    TopOn 
TopOn        
↾t                          |
73 | 72 | expimpd 608 |
. . . . 5
   TopOn  TopOn  
  
 
  
↾t        
 
  
           |
74 | 73 | rexlimdvva 2886 |
. . . 4
  TopOn  TopOn  
 
  
  ↾t 
                       |
75 | 9, 74 | syl5bi 221 |
. . 3
  TopOn  TopOn  
      ↾t          
 
  
           |
76 | 75 | ralrimiv 2800 |
. 2
  TopOn  TopOn  
      ↾t          
                |
77 | | simpr 463 |
. . 3
  TopOn  TopOn  
TopOn    |
78 | | ovex 6318 |
. . . . . 6
   |
79 | 78 | pwex 4586 |
. . . . 5
    |
80 | 5, 6, 7 | xkotf 20600 |
. . . . . 6
     ↾t                    ↾t          |
81 | | frn 5735 |
. . . . . 6
      ↾t                    ↾t            
 ↾t          
 
     |
82 | 80, 81 | ax-mp 5 |
. . . . 5
     ↾t                 |
83 | 79, 82 | ssexi 4548 |
. . . 4
     ↾t              |
84 | 83 | a1i 11 |
. . 3
  TopOn  TopOn  
     ↾t               |
85 | | topontop 19941 |
. . . 4
 TopOn 
  |
86 | | topontop 19941 |
. . . 4
 TopOn 
  |
87 | 5, 6, 7 | xkoval 20602 |
. . . 4
 
              
 ↾t          
      |
88 | 85, 86, 87 | syl2an 480 |
. . 3
  TopOn  TopOn  
             
 ↾t          
      |
89 | | eqid 2451 |
. . . . 5
         |
90 | 89 | xkotopon 20615 |
. . . 4
 
     TopOn      |
91 | 85, 86, 90 | syl2an 480 |
. . 3
  TopOn  TopOn  
    TopOn 
    |
92 | 77, 84, 88, 91 | subbascn 20270 |
. 2
  TopOn  TopOn  
            
             
     ↾t                             |
93 | 4, 76, 92 | mpbir2and 933 |
1
  TopOn  TopOn  

             |