Proof of Theorem cnntr
Step | Hyp | Ref
| Expression |
1 | | cnf2 12155 |
. . . 4
  TopOn  TopOn 
         |
2 | 1 | 3expia 1151 |
. . 3
  TopOn  TopOn  
  
       |
3 | | elpwi 3466 |
. . . . . . 7
    |
4 | 3 | adantl 273 |
. . . . . 6
   TopOn  TopOn  
    |
5 | | toponuni 11964 |
. . . . . . 7
 TopOn 
   |
6 | 5 | ad2antlr 476 |
. . . . . 6
   TopOn  TopOn  
     |
7 | 4, 6 | sseqtrd 3085 |
. . . . 5
   TopOn  TopOn  
     |
8 | | eqid 2100 |
. . . . . . 7
   |
9 | 8 | cnntri 12174 |
. . . . . 6
                  
               |
10 | 9 | expcom 115 |
. . . . 5
  
                               |
11 | 7, 10 | syl 14 |
. . . 4
   TopOn  TopOn  
  
                               |
12 | 11 | ralrimdva 2471 |
. . 3
  TopOn  TopOn  
  
                               |
13 | 2, 12 | jcad 303 |
. 2
  TopOn  TopOn  
  
     
             
                 |
14 | | toponss 11975 |
. . . . . . . . . 10
  TopOn     |
15 | | selpw 3464 |
. . . . . . . . . 10
 
  |
16 | 14, 15 | sylibr 133 |
. . . . . . . . 9
  TopOn      |
17 | 16 | ex 114 |
. . . . . . . 8
 TopOn 

    |
18 | 17 | ad2antlr 476 |
. . . . . . 7
   TopOn  TopOn  
     
    |
19 | 18 | imim1d 75 |
. . . . . 6
   TopOn  TopOn  
                    
                           
                 |
20 | | topontop 11963 |
. . . . . . . . . . 11
 TopOn 
  |
21 | 20 | ad3antrrr 479 |
. . . . . . . . . 10
    TopOn 
TopOn        
  |
22 | | cnvimass 4838 |
. . . . . . . . . . 11
    
 |
23 | | fdm 5214 |
. . . . . . . . . . . . 13
       |
24 | 23 | ad2antlr 476 |
. . . . . . . . . . . 12
    TopOn 
TopOn        
  |
25 | | toponuni 11964 |
. . . . . . . . . . . . 13
 TopOn 
   |
26 | 25 | ad3antrrr 479 |
. . . . . . . . . . . 12
    TopOn 
TopOn        
   |
27 | 24, 26 | eqtrd 2132 |
. . . . . . . . . . 11
    TopOn 
TopOn        
   |
28 | 22, 27 | syl5sseq 3097 |
. . . . . . . . . 10
    TopOn 
TopOn        
        |
29 | | eqid 2100 |
. . . . . . . . . . 11
   |
30 | 29 | ntrss2 12072 |
. . . . . . . . . 10
                             |
31 | 21, 28, 30 | syl2anc 406 |
. . . . . . . . 9
    TopOn 
TopOn        
            
       |
32 | | eqss 3062 |
. . . . . . . . . 10
                  
                                        |
33 | 32 | baib 872 |
. . . . . . . . 9
                                     
                     |
34 | 31, 33 | syl 14 |
. . . . . . . 8
    TopOn 
TopOn        
                  
                     |
35 | 29 | isopn3 12076 |
. . . . . . . . 9
                                    |
36 | 21, 28, 35 | syl2anc 406 |
. . . . . . . 8
    TopOn 
TopOn        
     
                     |
37 | | topontop 11963 |
. . . . . . . . . . . 12
 TopOn 
  |
38 | 37 | ad3antlr 480 |
. . . . . . . . . . 11
    TopOn 
TopOn        
  |
39 | | isopn3i 12086 |
. . . . . . . . . . 11
 
           |
40 | 38, 39 | sylancom 414 |
. . . . . . . . . 10
    TopOn 
TopOn        
          |
41 | 40 | imaeq2d 4817 |
. . . . . . . . 9
    TopOn 
TopOn        
                    |
42 | 41 | sseq1d 3076 |
. . . . . . . 8
    TopOn 
TopOn        
                                                |
43 | 34, 36, 42 | 3bitr4rd 220 |
. . . . . . 7
    TopOn 
TopOn        
                                   |
44 | 43 | pm5.74da 435 |
. . . . . 6
   TopOn  TopOn  
                   
             

         |
45 | 19, 44 | sylibd 148 |
. . . . 5
   TopOn  TopOn  
                    
                        |
46 | 45 | ralimdv2 2461 |
. . . 4
   TopOn  TopOn  
      
             
            

        |
47 | 46 | imdistanda 440 |
. . 3
  TopOn  TopOn  
                    
                             |
48 | | iscn 12147 |
. . 3
  TopOn  TopOn  
        
         |
49 | 47, 48 | sylibrd 168 |
. 2
  TopOn  TopOn  
                    
                   |
50 | 13, 49 | impbid 128 |
1
  TopOn  TopOn  
                                        |