Step | Hyp | Ref
| Expression |
1 | | isfcf 21049 |
. 2
  TopOn     
     
     




           |
2 | | simpll1 1047 |
. . . . . . . 8
    TopOn 
         
          
TopOn    |
3 | | topontop 19941 |
. . . . . . . 8
 TopOn 
  |
4 | 2, 3 | syl 17 |
. . . . . . 7
    TopOn 
         
          
  |
5 | | simpr 463 |
. . . . . . . 8
    TopOn 
         
          
            |
6 | | eqid 2451 |
. . . . . . . . 9
   |
7 | 6 | neii1 20122 |
. . . . . . . 8
 
              |
8 | 4, 5, 7 | syl2anc 667 |
. . . . . . 7
    TopOn 
         
              |
9 | 6 | ntrss2 20072 |
. . . . . . 7
           
  |
10 | 4, 8, 9 | syl2anc 667 |
. . . . . 6
    TopOn 
         
                     |
11 | | simplr 762 |
. . . . . . . . . . . 12
    TopOn 
         
          
  |
12 | | toponuni 19942 |
. . . . . . . . . . . . 13
 TopOn 
   |
13 | 2, 12 | syl 17 |
. . . . . . . . . . . 12
    TopOn 
         
          
   |
14 | 11, 13 | eleqtrd 2531 |
. . . . . . . . . . 11
    TopOn 
         
          
   |
15 | 14 | snssd 4117 |
. . . . . . . . . 10
    TopOn 
         
                |
16 | 6 | neiint 20120 |
. . . . . . . . . 10
    
 
          
             |
17 | 4, 15, 8, 16 | syl3anc 1268 |
. . . . . . . . 9
    TopOn 
         
                     
             |
18 | 5, 17 | mpbid 214 |
. . . . . . . 8
    TopOn 
         
                       |
19 | | snssg 4105 |
. . . . . . . . 9
 
       
             |
20 | 11, 19 | syl 17 |
. . . . . . . 8
    TopOn 
         
                                 |
21 | 18, 20 | mpbird 236 |
. . . . . . 7
    TopOn 
         
          
          |
22 | 6 | ntropn 20064 |
. . . . . . . . 9
              |
23 | 4, 8, 22 | syl2anc 667 |
. . . . . . . 8
    TopOn 
         
                     |
24 | | eleq2 2518 |
. . . . . . . . . 10
        

           |
25 | | ineq1 3627 |
. . . . . . . . . . . 12
        
                      |
26 | 25 | neeq1d 2683 |
. . . . . . . . . . 11
        
 
             
        |
27 | 26 | ralbidv 2827 |
. . . . . . . . . 10
        
 

              
        |
28 | 24, 27 | imbi12d 322 |
. . . . . . . . 9
        
 
       
                  
         |
29 | 28 | rspcv 3146 |
. . . . . . . 8
        
 

        
        
                  |
30 | 23, 29 | syl 17 |
. . . . . . 7
    TopOn 
         
             

                         
         |
31 | 21, 30 | mpid 42 |
. . . . . 6
    TopOn 
         
             

       
        
        |
32 | | ssrin 3657 |
. . . . . . . 8
        
              
       |
33 | | ssn0 3767 |
. . . . . . . . 9
          
     
                            |
34 | 33 | ex 436 |
. . . . . . . 8
               
                    
        |
35 | 32, 34 | syl 17 |
. . . . . . 7
        
               
        |
36 | 35 | ralimdv 2798 |
. . . . . 6
        
 
              
         |
37 | 10, 31, 36 | sylsyld 58 |
. . . . 5
    TopOn 
         
             

       

        |
38 | 37 | ralrimdva 2806 |
. . . 4
   TopOn     
       

                    
         |
39 | | simpl1 1011 |
. . . . . . . . . 10
   TopOn     
      TopOn    |
40 | 39, 3 | syl 17 |
. . . . . . . . 9
   TopOn     
        |
41 | | opnneip 20135 |
. . . . . . . . . 10
 
             |
42 | 41 | 3expb 1209 |
. . . . . . . . 9
  
              |
43 | 40, 42 | sylan 474 |
. . . . . . . 8
    TopOn 
         

              |
44 | | ineq1 3627 |
. . . . . . . . . . 11
 
             |
45 | 44 | neeq1d 2683 |
. . . . . . . . . 10
                 |
46 | 45 | ralbidv 2827 |
. . . . . . . . 9
  

               |
47 | 46 | rspcv 3146 |
. . . . . . . 8
            
           
      
         |
48 | 43, 47 | syl 17 |
. . . . . . 7
    TopOn 
         

               
      
         |
49 | 48 | expr 620 |
. . . . . 6
    TopOn 
         
 
             
      
          |
50 | 49 | com23 81 |
. . . . 5
    TopOn 
         
  
           
      
           |
51 | 50 | ralrimdva 2806 |
. . . 4
   TopOn     
       
           
      


          |
52 | 38, 51 | impbid 194 |
. . 3
   TopOn     
       

       
            
         |
53 | 52 | pm5.32da 647 |
. 2
  TopOn     
        
        

            
          |
54 | 1, 53 | bitrd 257 |
1
  TopOn     
     
     

            
          |