Step | Hyp | Ref
| Expression |
1 | | elflim 20986 |
. 2
  TopOn       
 

              |
2 | | dfss3 3422 |
. . . 4
                         |
3 | | topontop 19941 |
. . . . . . . . . . 11
 TopOn 
  |
4 | 3 | ad2antrr 732 |
. . . . . . . . . 10
   TopOn          |
5 | | opnneip 20135 |
. . . . . . . . . . 11
 
             |
6 | 5 | 3expb 1209 |
. . . . . . . . . 10
  
              |
7 | 4, 6 | sylan 474 |
. . . . . . . . 9
    TopOn 
     

 
            |
8 | | eleq1 2517 |
. . . . . . . . . 10
 
   |
9 | 8 | rspcv 3146 |
. . . . . . . . 9
            
          
   |
10 | 7, 9 | syl 17 |
. . . . . . . 8
    TopOn 
     

              
   |
11 | 10 | expr 620 |
. . . . . . 7
    TopOn 
     
 
            
    |
12 | 11 | com23 81 |
. . . . . 6
    TopOn 
     
  
          

    |
13 | 12 | ralrimdva 2806 |
. . . . 5
   TopOn         
          


    |
14 | | simpr 463 |
. . . . . . . . . 10
    TopOn 
     
                       |
15 | 3 | ad3antrrr 736 |
. . . . . . . . . . 11
    TopOn 
     
          
  |
16 | | simplr 762 |
. . . . . . . . . . . . 13
    TopOn 
     
          
  |
17 | | toponuni 19942 |
. . . . . . . . . . . . . 14
 TopOn 
   |
18 | 17 | ad3antrrr 736 |
. . . . . . . . . . . . 13
    TopOn 
     
          
   |
19 | 16, 18 | eleqtrd 2531 |
. . . . . . . . . . . 12
    TopOn 
     
          
   |
20 | 19 | snssd 4117 |
. . . . . . . . . . 11
    TopOn 
     
                |
21 | | eqid 2451 |
. . . . . . . . . . . . 13
   |
22 | 21 | neii1 20122 |
. . . . . . . . . . . 12
 
              |
23 | 4, 22 | sylan 474 |
. . . . . . . . . . 11
    TopOn 
     
          
   |
24 | 21 | neiint 20120 |
. . . . . . . . . . 11
    
 
          
             |
25 | 15, 20, 23, 24 | syl3anc 1268 |
. . . . . . . . . 10
    TopOn 
     
                     
             |
26 | 14, 25 | mpbid 214 |
. . . . . . . . 9
    TopOn 
     
                       |
27 | | snssg 4105 |
. . . . . . . . . 10
 
       
             |
28 | 27 | ad2antlr 733 |
. . . . . . . . 9
    TopOn 
     
                                 |
29 | 26, 28 | mpbird 236 |
. . . . . . . 8
    TopOn 
     
          
          |
30 | 21 | ntropn 20064 |
. . . . . . . . . 10
              |
31 | 15, 23, 30 | syl2anc 667 |
. . . . . . . . 9
    TopOn 
     
                     |
32 | | eleq2 2518 |
. . . . . . . . . . 11
        

           |
33 | | eleq1 2517 |
. . . . . . . . . . 11
        

           |
34 | 32, 33 | imbi12d 322 |
. . . . . . . . . 10
        
 

                     |
35 | 34 | rspcv 3146 |
. . . . . . . . 9
        
 

                      |
36 | 31, 35 | syl 17 |
. . . . . . . 8
    TopOn 
     
             
 
                    |
37 | 29, 36 | mpid 42 |
. . . . . . 7
    TopOn 
     
             
            |
38 | | simpllr 769 |
. . . . . . . 8
    TopOn 
     
          
      |
39 | 21 | ntrss2 20072 |
. . . . . . . . 9
           
  |
40 | 15, 23, 39 | syl2anc 667 |
. . . . . . . 8
    TopOn 
     
                     |
41 | 23, 18 | sseqtr4d 3469 |
. . . . . . . 8
    TopOn 
     
          
  |
42 | | filss 20868 |
. . . . . . . . . 10
              
            |
43 | 42 | 3exp2 1227 |
. . . . . . . . 9
    
        
         
     |
44 | 43 | com24 90 |
. . . . . . . 8
    
        

        
     |
45 | 38, 40, 41, 44 | syl3c 63 |
. . . . . . 7
    TopOn 
     
                       |
46 | 37, 45 | syld 45 |
. . . . . 6
    TopOn 
     
             
    |
47 | 46 | ralrimdva 2806 |
. . . . 5
   TopOn         

                |
48 | 13, 47 | impbid 194 |
. . . 4
   TopOn         
            
    |
49 | 2, 48 | syl5bb 261 |
. . 3
   TopOn                    
    |
50 | 49 | pm5.32da 647 |
. 2
  TopOn                     

     |
51 | 1, 50 | bitrd 257 |
1
  TopOn       
 



     |