Proof of Theorem cncls2
Step | Hyp | Ref
| Expression |
1 | | cnf2 20265 |
. . . 4
  TopOn  TopOn 
         |
2 | 1 | 3expia 1210 |
. . 3
  TopOn  TopOn  
  
       |
3 | | elpwi 3960 |
. . . . . . 7
    |
4 | 3 | adantl 468 |
. . . . . 6
   TopOn  TopOn  
    |
5 | | toponuni 19942 |
. . . . . . 7
 TopOn 
   |
6 | 5 | ad2antlr 733 |
. . . . . 6
   TopOn  TopOn  
     |
7 | 4, 6 | sseqtrd 3468 |
. . . . 5
   TopOn  TopOn  
     |
8 | | eqid 2451 |
. . . . . . 7
   |
9 | 8 | cncls2i 20286 |
. . . . . 6
                  
               |
10 | 9 | expcom 437 |
. . . . 5
  
                               |
11 | 7, 10 | syl 17 |
. . . 4
   TopOn  TopOn  
  
                               |
12 | 11 | ralrimdva 2806 |
. . 3
  TopOn  TopOn  
  
                               |
13 | 2, 12 | jcad 536 |
. 2
  TopOn  TopOn  
  
     
                               |
14 | 8 | cldss2 20045 |
. . . . . . . . 9
       |
15 | 5 | ad2antlr 733 |
. . . . . . . . . 10
   TopOn  TopOn  
        |
16 | 15 | pweqd 3956 |
. . . . . . . . 9
   TopOn  TopOn  
     
    |
17 | 14, 16 | syl5sseqr 3481 |
. . . . . . . 8
   TopOn  TopOn  
            |
18 | 17 | sseld 3431 |
. . . . . . 7
   TopOn  TopOn  
              |
19 | 18 | imim1d 78 |
. . . . . 6
   TopOn  TopOn  
                    
                                                 |
20 | | cldcls 20057 |
. . . . . . . . . . . 12
    
          |
21 | 20 | ad2antll 735 |
. . . . . . . . . . 11
   TopOn  TopOn  
                     |
22 | 21 | imaeq2d 5168 |
. . . . . . . . . 10
   TopOn  TopOn  
                               |
23 | 22 | sseq2d 3460 |
. . . . . . . . 9
   TopOn  TopOn  
                        
            
            
        |
24 | | topontop 19941 |
. . . . . . . . . . 11
 TopOn 
  |
25 | 24 | ad2antrr 732 |
. . . . . . . . . 10
   TopOn  TopOn  
          
  |
26 | | cnvimass 5188 |
. . . . . . . . . . 11
    
 |
27 | | fdm 5733 |
. . . . . . . . . . . . 13
       |
28 | 27 | ad2antrl 734 |
. . . . . . . . . . . 12
   TopOn  TopOn  
             |
29 | | toponuni 19942 |
. . . . . . . . . . . . 13
 TopOn 
   |
30 | 29 | ad2antrr 732 |
. . . . . . . . . . . 12
   TopOn  TopOn  
          
   |
31 | 28, 30 | eqtrd 2485 |
. . . . . . . . . . 11
   TopOn  TopOn  
              |
32 | 26, 31 | syl5sseq 3480 |
. . . . . . . . . 10
   TopOn  TopOn  
                   |
33 | | eqid 2451 |
. . . . . . . . . . 11
   |
34 | 33 | iscld4 20081 |
. . . . . . . . . 10
                                        |
35 | 25, 32, 34 | syl2anc 667 |
. . . . . . . . 9
   TopOn  TopOn  
                                          |
36 | 23, 35 | bitr4d 260 |
. . . . . . . 8
   TopOn  TopOn  
                        
            
            |
37 | 36 | expr 620 |
. . . . . . 7
   TopOn  TopOn  
                                                  |
38 | 37 | pm5.74d 251 |
. . . . . 6
   TopOn  TopOn  
                                     
    
             |
39 | 19, 38 | sylibd 218 |
. . . . 5
   TopOn  TopOn  
                    
                                |
40 | 39 | ralimdv2 2795 |
. . . 4
   TopOn  TopOn  
      
             
                               |
41 | 40 | imdistanda 699 |
. . 3
  TopOn  TopOn  
                                                           |
42 | | iscncl 20285 |
. . 3
  TopOn  TopOn  
                           |
43 | 41, 42 | sylibrd 238 |
. 2
  TopOn  TopOn  
                                        |
44 | 13, 43 | impbid 194 |
1
  TopOn  TopOn  
                                        |