Step | Hyp | Ref
| Expression |
1 | | cnpf2 20343 |
. . . . . 6
  TopOn  TopOn 
      
      |
2 | 1 | 3expa 1231 |
. . . . 5
   TopOn  TopOn  
      
      |
3 | 2 | 3adantl3 1188 |
. . . 4
   TopOn  TopOn 

      
      |
4 | | simplr 770 |
. . . . . . 7
    TopOn 
TopOn                        
        |
5 | | simpll2 1070 |
. . . . . . . . 9
    TopOn 
TopOn                        
TopOn    |
6 | | topontop 20018 |
. . . . . . . . 9
 TopOn 
  |
7 | 5, 6 | syl 17 |
. . . . . . . 8
    TopOn 
TopOn                        
  |
8 | | eqid 2471 |
. . . . . . . . . 10
   |
9 | 8 | neii1 20199 |
. . . . . . . . 9
 
              
   |
10 | 7, 9 | sylancom 680 |
. . . . . . . 8
    TopOn 
TopOn                        
   |
11 | 8 | ntropn 20141 |
. . . . . . . 8
              |
12 | 7, 10, 11 | syl2anc 673 |
. . . . . . 7
    TopOn 
TopOn                                   |
13 | | simpr 468 |
. . . . . . . . 9
    TopOn 
TopOn                                         |
14 | 3 | adantr 472 |
. . . . . . . . . . . . 13
    TopOn 
TopOn                               |
15 | | simpll3 1071 |
. . . . . . . . . . . . 13
    TopOn 
TopOn                        
  |
16 | 14, 15 | ffvelrnd 6038 |
. . . . . . . . . . . 12
    TopOn 
TopOn                               |
17 | | toponuni 20019 |
. . . . . . . . . . . . 13
 TopOn 
   |
18 | 5, 17 | syl 17 |
. . . . . . . . . . . 12
    TopOn 
TopOn                        
   |
19 | 16, 18 | eleqtrd 2551 |
. . . . . . . . . . 11
    TopOn 
TopOn                                |
20 | 19 | snssd 4108 |
. . . . . . . . . 10
    TopOn 
TopOn                                  |
21 | 8 | neiint 20197 |
. . . . . . . . . 10
        
 
              
                 |
22 | 7, 20, 10, 21 | syl3anc 1292 |
. . . . . . . . 9
    TopOn 
TopOn                                       
                 |
23 | 13, 22 | mpbid 215 |
. . . . . . . 8
    TopOn 
TopOn                                         |
24 | | fvex 5889 |
. . . . . . . . 9
     |
25 | 24 | snss 4087 |
. . . . . . . 8
                             |
26 | 23, 25 | sylibr 217 |
. . . . . . 7
    TopOn 
TopOn                                       |
27 | | cnpimaex 20349 |
. . . . . . 7
               
            


               |
28 | 4, 12, 26, 27 | syl3anc 1292 |
. . . . . 6
    TopOn 
TopOn                         

   
           |
29 | | simpl1 1033 |
. . . . . . . . . . . 12
   TopOn  TopOn 

      
TopOn    |
30 | 29 | ad2antrr 740 |
. . . . . . . . . . 11
     TopOn 
TopOn 

      
               
    
          
TopOn    |
31 | | topontop 20018 |
. . . . . . . . . . 11
 TopOn 
  |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
  |
33 | | simprl 772 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
  |
34 | | simprrl 782 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
  |
35 | | opnneip 20212 |
. . . . . . . . . 10
 
             |
36 | 32, 33, 34, 35 | syl3anc 1292 |
. . . . . . . . 9
     TopOn 
TopOn 

      
               
    
          
            |
37 | | simprrr 783 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
              |
38 | 8 | ntrss2 20149 |
. . . . . . . . . . . 12
           
  |
39 | 7, 10, 38 | syl2anc 673 |
. . . . . . . . . . 11
    TopOn 
TopOn                                   |
40 | 39 | adantr 472 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
          |
41 | 37, 40 | sstrd 3428 |
. . . . . . . . 9
     TopOn 
TopOn 

      
               
    
          
      |
42 | 36, 41 | jca 541 |
. . . . . . . 8
     TopOn 
TopOn 

      
               
    
          
                  |
43 | 42 | ex 441 |
. . . . . . 7
    TopOn 
TopOn                                                    
        |
44 | 43 | reximdv2 2855 |
. . . . . 6
    TopOn 
TopOn                                        
                   |
45 | 28, 44 | mpd 15 |
. . . . 5
    TopOn 
TopOn                         
                 |
46 | 45 | ralrimiva 2809 |
. . . 4
   TopOn  TopOn 

      
                                  |
47 | 3, 46 | jca 541 |
. . 3
   TopOn  TopOn 

      
     
                                  |
48 | 47 | ex 441 |
. 2
  TopOn  TopOn 

                                                |
49 | | simpll2 1070 |
. . . . . . . . . . 11
    TopOn 
TopOn              
TopOn    |
50 | 49, 6 | syl 17 |
. . . . . . . . . 10
    TopOn 
TopOn              
  |
51 | | simprl 772 |
. . . . . . . . . 10
    TopOn 
TopOn              
  |
52 | | simprr 774 |
. . . . . . . . . 10
    TopOn 
TopOn              
      |
53 | | opnneip 20212 |
. . . . . . . . . 10
 
                     |
54 | 50, 51, 52, 53 | syl3anc 1292 |
. . . . . . . . 9
    TopOn 
TopOn              
                |
55 | | simpl1 1033 |
. . . . . . . . . . . . . 14
   TopOn  TopOn 

     TopOn    |
56 | 55 | ad2antrr 740 |
. . . . . . . . . . . . 13
     TopOn 
TopOn 
             
               
TopOn    |
57 | 56, 31 | syl 17 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
               
  |
58 | | simprl 772 |
. . . . . . . . . . . . 13
     TopOn 
TopOn 
             
               
            |
59 | | eqid 2471 |
. . . . . . . . . . . . . 14
   |
60 | 59 | neii1 20199 |
. . . . . . . . . . . . 13
 
              |
61 | 57, 58, 60 | syl2anc 673 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                   |
62 | 59 | ntropn 20141 |
. . . . . . . . . . . 12
              |
63 | 57, 61, 62 | syl2anc 673 |
. . . . . . . . . . 11
     TopOn 
TopOn 
             
                          |
64 | | simpll3 1071 |
. . . . . . . . . . . . . . . . 17
    TopOn 
TopOn              
  |
65 | 64 | adantr 472 |
. . . . . . . . . . . . . . . 16
     TopOn 
TopOn 
             
               
  |
66 | | toponuni 20019 |
. . . . . . . . . . . . . . . . 17
 TopOn 
   |
67 | 56, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
     TopOn 
TopOn 
             
               
   |
68 | 65, 67 | eleqtrd 2551 |
. . . . . . . . . . . . . . 15
     TopOn 
TopOn 
             
               
   |
69 | 68 | snssd 4108 |
. . . . . . . . . . . . . 14
     TopOn 
TopOn 
             
                     |
70 | 59 | neiint 20197 |
. . . . . . . . . . . . . 14
    
 
          
             |
71 | 57, 69, 61, 70 | syl3anc 1292 |
. . . . . . . . . . . . 13
     TopOn 
TopOn 
             
                          
             |
72 | 58, 71 | mpbid 215 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                            |
73 | | snssg 4096 |
. . . . . . . . . . . . 13
 
       
             |
74 | 65, 73 | syl 17 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                                      |
75 | 72, 74 | mpbird 240 |
. . . . . . . . . . 11
     TopOn 
TopOn 
             
               
          |
76 | 59 | ntrss2 20149 |
. . . . . . . . . . . . . 14
           
  |
77 | 57, 61, 76 | syl2anc 673 |
. . . . . . . . . . . . 13
     TopOn 
TopOn 
             
                          |
78 | | imass2 5210 |
. . . . . . . . . . . . 13
        
           
      |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                           
      |
80 | | simprr 774 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                   
  |
81 | 79, 80 | sstrd 3428 |
. . . . . . . . . . 11
     TopOn 
TopOn 
             
                           
  |
82 | | eleq2 2538 |
. . . . . . . . . . . . 13
        

           |
83 | | imaeq2 5170 |
. . . . . . . . . . . . . 14
        
                  |
84 | 83 | sseq1d 3445 |
. . . . . . . . . . . . 13
        
                
   |
85 | 82, 84 | anbi12d 725 |
. . . . . . . . . . . 12
        
 
    
                    
    |
86 | 85 | rspcev 3136 |
. . . . . . . . . . 11
         

                      

       |
87 | 63, 75, 81, 86 | syl12anc 1290 |
. . . . . . . . . 10
     TopOn 
TopOn 
             
                

   
   |
88 | 87 | rexlimdvaa 2872 |
. . . . . . . . 9
    TopOn 
TopOn              
 
               

        |
89 | 54, 88 | embantd 55 |
. . . . . . . 8
    TopOn 
TopOn              
               
                 

        |
90 | 89 | ex 441 |
. . . . . . 7
   TopOn  TopOn 

                            
                

         |
91 | 90 | com23 80 |
. . . . . 6
   TopOn  TopOn 

                                              
   
     |
92 | 91 | exp4a 617 |
. . . . 5
   TopOn  TopOn 

                                             
   
      |
93 | 92 | ralimdv2 2804 |
. . . 4
   TopOn  TopOn 

      
                                      
   
     |
94 | 93 | imdistanda 707 |
. . 3
  TopOn  TopOn 

                                                  

   
      |
95 | | iscnp 20330 |
. . 3
  TopOn  TopOn 

                 


          |
96 | 94, 95 | sylibrd 242 |
. 2
  TopOn  TopOn 

                                                |
97 | 48, 96 | impbid 195 |
1
  TopOn  TopOn 

                                                |