Proof of Theorem cncls2
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 | ad2antlr 741 |
. . . . . 6
   TopOn  TopOn  
     |
7 | 4, 6 | sseqtrd 3454 |
. . . . 5
   TopOn  TopOn  
     |
8 | | eqid 2471 |
. . . . . . 7
   |
9 | 8 | cncls2i 20363 |
. . . . . 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 | 8 | cldss2 20122 |
. . . . . . . . 9
       |
15 | 5 | ad2antlr 741 |
. . . . . . . . . 10
   TopOn  TopOn  
        |
16 | 15 | pweqd 3947 |
. . . . . . . . 9
   TopOn  TopOn  
     
    |
17 | 14, 16 | syl5sseqr 3467 |
. . . . . . . 8
   TopOn  TopOn  
            |
18 | 17 | sseld 3417 |
. . . . . . 7
   TopOn  TopOn  
              |
19 | 18 | imim1d 77 |
. . . . . 6
   TopOn  TopOn  
                    
                                                 |
20 | | cldcls 20134 |
. . . . . . . . . . . 12
    
          |
21 | 20 | ad2antll 743 |
. . . . . . . . . . 11
   TopOn  TopOn  
                     |
22 | 21 | imaeq2d 5174 |
. . . . . . . . . 10
   TopOn  TopOn  
                               |
23 | 22 | sseq2d 3446 |
. . . . . . . . 9
   TopOn  TopOn  
                        
            
            
        |
24 | | topontop 20018 |
. . . . . . . . . . 11
 TopOn 
  |
25 | 24 | ad2antrr 740 |
. . . . . . . . . 10
   TopOn  TopOn  
          
  |
26 | | cnvimass 5194 |
. . . . . . . . . . 11
    
 |
27 | | fdm 5745 |
. . . . . . . . . . . . 13
       |
28 | 27 | ad2antrl 742 |
. . . . . . . . . . . 12
   TopOn  TopOn  
             |
29 | | toponuni 20019 |
. . . . . . . . . . . . 13
 TopOn 
   |
30 | 29 | ad2antrr 740 |
. . . . . . . . . . . 12
   TopOn  TopOn  
          
   |
31 | 28, 30 | eqtrd 2505 |
. . . . . . . . . . 11
   TopOn  TopOn  
              |
32 | 26, 31 | syl5sseq 3466 |
. . . . . . . . . 10
   TopOn  TopOn  
                   |
33 | | eqid 2471 |
. . . . . . . . . . 11
   |
34 | 33 | iscld4 20158 |
. . . . . . . . . 10
                                        |
35 | 25, 32, 34 | syl2anc 673 |
. . . . . . . . 9
   TopOn  TopOn  
                                          |
36 | 23, 35 | bitr4d 264 |
. . . . . . . 8
   TopOn  TopOn  
                        
            
            |
37 | 36 | expr 626 |
. . . . . . 7
   TopOn  TopOn  
                                                  |
38 | 37 | pm5.74d 255 |
. . . . . 6
   TopOn  TopOn  
                                     
    
             |
39 | 19, 38 | sylibd 222 |
. . . . 5
   TopOn  TopOn  
                    
                                |
40 | 39 | ralimdv2 2804 |
. . . 4
   TopOn  TopOn  
      
             
                               |
41 | 40 | imdistanda 707 |
. . 3
  TopOn  TopOn  
                                                           |
42 | | iscncl 20362 |
. . 3
  TopOn  TopOn  
                           |
43 | 41, 42 | sylibrd 242 |
. 2
  TopOn  TopOn  
                                        |
44 | 13, 43 | impbid 195 |
1
  TopOn  TopOn  
                                        |