Proof of Theorem cnntr
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 | cnntri 20287 |
. . . . . 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 | | toponss 19944 |
. . . . . . . . . 10
  TopOn     |
15 | | selpw 3958 |
. . . . . . . . . 10
 
  |
16 | 14, 15 | sylibr 216 |
. . . . . . . . 9
  TopOn      |
17 | 16 | ex 436 |
. . . . . . . 8
 TopOn 

    |
18 | 17 | ad2antlr 733 |
. . . . . . 7
   TopOn  TopOn  
     
    |
19 | 18 | imim1d 78 |
. . . . . 6
   TopOn  TopOn  
                    
                           
                 |
20 | | topontop 19941 |
. . . . . . . . . . 11
 TopOn 
  |
21 | 20 | ad3antrrr 736 |
. . . . . . . . . 10
    TopOn 
TopOn        
  |
22 | | cnvimass 5188 |
. . . . . . . . . . 11
    
 |
23 | | fdm 5733 |
. . . . . . . . . . . . 13
       |
24 | 23 | ad2antlr 733 |
. . . . . . . . . . . 12
    TopOn 
TopOn        
  |
25 | | toponuni 19942 |
. . . . . . . . . . . . 13
 TopOn 
   |
26 | 25 | ad3antrrr 736 |
. . . . . . . . . . . 12
    TopOn 
TopOn        
   |
27 | 24, 26 | eqtrd 2485 |
. . . . . . . . . . 11
    TopOn 
TopOn        
   |
28 | 22, 27 | syl5sseq 3480 |
. . . . . . . . . 10
    TopOn 
TopOn        
        |
29 | | eqid 2451 |
. . . . . . . . . . 11
   |
30 | 29 | ntrss2 20072 |
. . . . . . . . . 10
                             |
31 | 21, 28, 30 | syl2anc 667 |
. . . . . . . . 9
    TopOn 
TopOn        
            
       |
32 | | eqss 3447 |
. . . . . . . . . 10
                  
                                        |
33 | 32 | baib 914 |
. . . . . . . . 9
                                     
                     |
34 | 31, 33 | syl 17 |
. . . . . . . 8
    TopOn 
TopOn        
                  
                     |
35 | 29 | isopn3 20082 |
. . . . . . . . 9
                                    |
36 | 21, 28, 35 | syl2anc 667 |
. . . . . . . 8
    TopOn 
TopOn        
     
                     |
37 | | topontop 19941 |
. . . . . . . . . . . 12
 TopOn 
  |
38 | 37 | ad3antlr 737 |
. . . . . . . . . . 11
    TopOn 
TopOn        
  |
39 | | isopn3i 20098 |
. . . . . . . . . . 11
 
           |
40 | 38, 39 | sylancom 673 |
. . . . . . . . . 10
    TopOn 
TopOn        
          |
41 | 40 | imaeq2d 5168 |
. . . . . . . . 9
    TopOn 
TopOn        
                    |
42 | 41 | sseq1d 3459 |
. . . . . . . 8
    TopOn 
TopOn        
                                                |
43 | 34, 36, 42 | 3bitr4rd 290 |
. . . . . . 7
    TopOn 
TopOn        
                                   |
44 | 43 | pm5.74da 693 |
. . . . . 6
   TopOn  TopOn  
                   
             

         |
45 | 19, 44 | sylibd 218 |
. . . . 5
   TopOn  TopOn  
                    
                        |
46 | 45 | ralimdv2 2795 |
. . . 4
   TopOn  TopOn  
      
             
            

        |
47 | 46 | imdistanda 699 |
. . 3
  TopOn  TopOn  
                    
                             |
48 | | iscn 20251 |
. . 3
  TopOn  TopOn  
        
         |
49 | 47, 48 | sylibrd 238 |
. 2
  TopOn  TopOn  
                    
                   |
50 | 13, 49 | impbid 194 |
1
  TopOn  TopOn  
                                        |