Step | Hyp | Ref
| Expression |
1 | | cnf2 20342 |
. . . 4
  TopOn  TopOn 
         |
2 | 1 | 3expia 1233 |
. . 3
  TopOn  TopOn  
  
       |
3 | | elpwi 3951 |
. . . . . . 7
    |
4 | 3 | adantl 473 |
. . . . . 6
   TopOn  TopOn  
    |
5 | | toponuni 20019 |
. . . . . . 7
 TopOn 
   |
6 | 5 | ad2antrr 740 |
. . . . . 6
   TopOn  TopOn  
     |
7 | 4, 6 | sseqtrd 3454 |
. . . . 5
   TopOn  TopOn  
     |
8 | | eqid 2471 |
. . . . . . 7
   |
9 | 8 | cnclsi 20365 |
. . . . . 6
                 
              |
10 | 9 | expcom 442 |
. . . . 5
  
                             |
11 | 7, 10 | syl 17 |
. . . 4
   TopOn  TopOn  
  
                             |
12 | 11 | ralrimdva 2812 |
. . 3
  TopOn  TopOn  
  
                             |
13 | 2, 12 | jcad 542 |
. 2
  TopOn  TopOn  
  
     
            
                |
14 | | cnvimass 5194 |
. . . . . . . . 9
    
 |
15 | | fdm 5745 |
. . . . . . . . . 10
       |
16 | 15 | ad2antlr 741 |
. . . . . . . . 9
    TopOn 
TopOn            |
17 | 14, 16 | syl5sseq 3466 |
. . . . . . . 8
    TopOn 
TopOn                 |
18 | | toponmax 20020 |
. . . . . . . . . 10
 TopOn 
  |
19 | 18 | ad3antrrr 744 |
. . . . . . . . 9
    TopOn 
TopOn            |
20 | | elpw2g 4564 |
. . . . . . . . 9
                |
21 | 19, 20 | syl 17 |
. . . . . . . 8
    TopOn 
TopOn                         |
22 | 17, 21 | mpbird 240 |
. . . . . . 7
    TopOn 
TopOn                  |
23 | | fveq2 5879 |
. . . . . . . . . 10
                             |
24 | 23 | imaeq2d 5174 |
. . . . . . . . 9
                                     |
25 | | imaeq2 5170 |
. . . . . . . . . 10
                     |
26 | 25 | fveq2d 5883 |
. . . . . . . . 9
                                     |
27 | 24, 26 | sseq12d 3447 |
. . . . . . . 8
                  
                            
                    |
28 | 27 | rspcv 3132 |
. . . . . . 7
                                                  
                    |
29 | 22, 28 | syl 17 |
. . . . . 6
    TopOn 
TopOn           
            
           
                
                    |
30 | | topontop 20018 |
. . . . . . . . . 10
 TopOn 
  |
31 | 30 | ad3antlr 745 |
. . . . . . . . 9
    TopOn 
TopOn            |
32 | | elpwi 3951 |
. . . . . . . . . . 11
 
  |
33 | 32 | adantl 473 |
. . . . . . . . . 10
    TopOn 
TopOn            |
34 | | toponuni 20019 |
. . . . . . . . . . 11
 TopOn 
   |
35 | 34 | ad3antlr 745 |
. . . . . . . . . 10
    TopOn 
TopOn             |
36 | 33, 35 | sseqtrd 3454 |
. . . . . . . . 9
    TopOn 
TopOn             |
37 | | ffun 5742 |
. . . . . . . . . . . 12
       |
38 | 37 | ad2antlr 741 |
. . . . . . . . . . 11
    TopOn 
TopOn            |
39 | | funimacnv 5665 |
. . . . . . . . . . 11

             |
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
    TopOn 
TopOn                       |
41 | | inss1 3643 |
. . . . . . . . . 10

  |
42 | 40, 41 | syl6eqss 3468 |
. . . . . . . . 9
    TopOn 
TopOn                     |
43 | | eqid 2471 |
. . . . . . . . . 10
   |
44 | 43 | clsss 20146 |
. . . . . . . . 9
           
                            |
45 | 31, 36, 42, 44 | syl3anc 1292 |
. . . . . . . 8
    TopOn 
TopOn                                     |
46 | | sstr2 3425 |
. . . . . . . 8
                                                            
                
           |
47 | 45, 46 | syl5com 30 |
. . . . . . 7
    TopOn 
TopOn                           
                                             |
48 | | topontop 20018 |
. . . . . . . . . . 11
 TopOn 
  |
49 | 48 | ad3antrrr 744 |
. . . . . . . . . 10
    TopOn 
TopOn            |
50 | 5 | ad3antrrr 744 |
. . . . . . . . . . . 12
    TopOn 
TopOn             |
51 | 16, 50 | eqtrd 2505 |
. . . . . . . . . . 11
    TopOn 
TopOn             |
52 | 14, 51 | syl5sseq 3466 |
. . . . . . . . . 10
    TopOn 
TopOn                  |
53 | 8 | clsss3 20151 |
. . . . . . . . . 10
                         |
54 | 49, 52, 53 | syl2anc 673 |
. . . . . . . . 9
    TopOn 
TopOn                          |
55 | 54, 51 | sseqtr4d 3455 |
. . . . . . . 8
    TopOn 
TopOn                      
  |
56 | | funimass3 6013 |
. . . . . . . 8
              
                  
       
            
                |
57 | 38, 55, 56 | syl2anc 673 |
. . . . . . 7
    TopOn 
TopOn                           
       
            
                |
58 | 47, 57 | sylibd 222 |
. . . . . 6
    TopOn 
TopOn                           
                                              |
59 | 29, 58 | syld 44 |
. . . . 5
    TopOn 
TopOn           
            
           
            
                |
60 | 59 | ralrimdva 2812 |
. . . 4
   TopOn  TopOn  
      
            
           
                               |
61 | 60 | imdistanda 707 |
. . 3
  TopOn  TopOn  
                   
                                                  |
62 | | cncls2 20366 |
. . 3
  TopOn  TopOn  
                                        |
63 | 61, 62 | sylibrd 242 |
. 2
  TopOn  TopOn  
                   
                  |
64 | 13, 63 | impbid 195 |
1
  TopOn  TopOn  
                                      |