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

      
      |
4 | | simplr 754 |
. . . . . . 7
    TopOn 
TopOn                        
        |
5 | | simpll2 1028 |
. . . . . . . . 9
    TopOn 
TopOn                        
TopOn    |
6 | | topontop 18658 |
. . . . . . . . 9
 TopOn 
  |
7 | 5, 6 | syl 16 |
. . . . . . . 8
    TopOn 
TopOn                        
  |
8 | | eqid 2452 |
. . . . . . . . . 10
   |
9 | 8 | neii1 18837 |
. . . . . . . . 9
 
              
   |
10 | 7, 9 | sylancom 667 |
. . . . . . . 8
    TopOn 
TopOn                        
   |
11 | 8 | ntropn 18780 |
. . . . . . . 8
              |
12 | 7, 10, 11 | syl2anc 661 |
. . . . . . 7
    TopOn 
TopOn                                   |
13 | | simpr 461 |
. . . . . . . . 9
    TopOn 
TopOn                                         |
14 | 3 | adantr 465 |
. . . . . . . . . . . . 13
    TopOn 
TopOn                               |
15 | | simpll3 1029 |
. . . . . . . . . . . . 13
    TopOn 
TopOn                        
  |
16 | 14, 15 | ffvelrnd 5948 |
. . . . . . . . . . . 12
    TopOn 
TopOn                               |
17 | | toponuni 18659 |
. . . . . . . . . . . . 13
 TopOn 
   |
18 | 5, 17 | syl 16 |
. . . . . . . . . . . 12
    TopOn 
TopOn                        
   |
19 | 16, 18 | eleqtrd 2542 |
. . . . . . . . . . 11
    TopOn 
TopOn                                |
20 | 19 | snssd 4121 |
. . . . . . . . . 10
    TopOn 
TopOn                                  |
21 | 8 | neiint 18835 |
. . . . . . . . . 10
        
 
              
                 |
22 | 7, 20, 10, 21 | syl3anc 1219 |
. . . . . . . . 9
    TopOn 
TopOn                                       
                 |
23 | 13, 22 | mpbid 210 |
. . . . . . . 8
    TopOn 
TopOn                                         |
24 | | fvex 5804 |
. . . . . . . . 9
     |
25 | 24 | snss 4102 |
. . . . . . . 8
                             |
26 | 23, 25 | sylibr 212 |
. . . . . . 7
    TopOn 
TopOn                                       |
27 | | cnpimaex 18987 |
. . . . . . 7
               
            


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

   
           |
29 | | simpl1 991 |
. . . . . . . . . . . 12
   TopOn  TopOn 

      
TopOn    |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . 11
     TopOn 
TopOn 

      
               
    
          
TopOn    |
31 | | topontop 18658 |
. . . . . . . . . . 11
 TopOn 
  |
32 | 30, 31 | syl 16 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
  |
33 | | simprl 755 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
  |
34 | | simprrl 763 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
  |
35 | | opnneip 18850 |
. . . . . . . . . 10
 
             |
36 | 32, 33, 34, 35 | syl3anc 1219 |
. . . . . . . . 9
     TopOn 
TopOn 

      
               
    
          
            |
37 | | simprrr 764 |
. . . . . . . . . 10
     TopOn 
TopOn 

      
               
    
          
              |
38 | 8 | ntrss2 18788 |
. . . . . . . . . . . 12
           
  |
39 | 7, 10, 38 | syl2anc 661 |
. . . . . . . . . . 11
    TopOn 
TopOn                                   |
40 | 39 | adantr 465 |
. . . . . . . . . 10
     TopOn 
TopOn 

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

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

      
               
    
          
                  |
43 | 42 | ex 434 |
. . . . . . 7
    TopOn 
TopOn                                                    
        |
44 | 43 | reximdv2 2925 |
. . . . . 6
    TopOn 
TopOn                                        
                   |
45 | 28, 44 | mpd 15 |
. . . . 5
    TopOn 
TopOn                         
                 |
46 | 45 | ralrimiva 2827 |
. . . 4
   TopOn  TopOn 

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

      
     
                                  |
48 | 47 | ex 434 |
. 2
  TopOn  TopOn 

                                                |
49 | | simpll2 1028 |
. . . . . . . . . . 11
    TopOn 
TopOn              
TopOn    |
50 | 49, 6 | syl 16 |
. . . . . . . . . 10
    TopOn 
TopOn              
  |
51 | | simprl 755 |
. . . . . . . . . 10
    TopOn 
TopOn              
  |
52 | | simprr 756 |
. . . . . . . . . 10
    TopOn 
TopOn              
      |
53 | | opnneip 18850 |
. . . . . . . . . 10
 
                     |
54 | 50, 51, 52, 53 | syl3anc 1219 |
. . . . . . . . 9
    TopOn 
TopOn              
                |
55 | | simpl1 991 |
. . . . . . . . . . . . . 14
   TopOn  TopOn 

     TopOn    |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . . 13
     TopOn 
TopOn 
             
               
TopOn    |
57 | 56, 31 | syl 16 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
               
  |
58 | | simprl 755 |
. . . . . . . . . . . . 13
     TopOn 
TopOn 
             
               
            |
59 | | eqid 2452 |
. . . . . . . . . . . . . 14
   |
60 | 59 | neii1 18837 |
. . . . . . . . . . . . 13
 
              |
61 | 57, 58, 60 | syl2anc 661 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                   |
62 | 59 | ntropn 18780 |
. . . . . . . . . . . 12
              |
63 | 57, 61, 62 | syl2anc 661 |
. . . . . . . . . . 11
     TopOn 
TopOn 
             
                          |
64 | | simpll3 1029 |
. . . . . . . . . . . . . . . . 17
    TopOn 
TopOn              
  |
65 | 64 | adantr 465 |
. . . . . . . . . . . . . . . 16
     TopOn 
TopOn 
             
               
  |
66 | | toponuni 18659 |
. . . . . . . . . . . . . . . . 17
 TopOn 
   |
67 | 56, 66 | syl 16 |
. . . . . . . . . . . . . . . 16
     TopOn 
TopOn 
             
               
   |
68 | 65, 67 | eleqtrd 2542 |
. . . . . . . . . . . . . . 15
     TopOn 
TopOn 
             
               
   |
69 | 68 | snssd 4121 |
. . . . . . . . . . . . . 14
     TopOn 
TopOn 
             
                     |
70 | 59 | neiint 18835 |
. . . . . . . . . . . . . 14
    
 
          
             |
71 | 57, 69, 61, 70 | syl3anc 1219 |
. . . . . . . . . . . . 13
     TopOn 
TopOn 
             
                          
             |
72 | 58, 71 | mpbid 210 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                            |
73 | | snssg 4110 |
. . . . . . . . . . . . 13
 
       
             |
74 | 65, 73 | syl 16 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                                      |
75 | 72, 74 | mpbird 232 |
. . . . . . . . . . 11
     TopOn 
TopOn 
             
               
          |
76 | 59 | ntrss2 18788 |
. . . . . . . . . . . . . 14
           
  |
77 | 57, 61, 76 | syl2anc 661 |
. . . . . . . . . . . . 13
     TopOn 
TopOn 
             
                          |
78 | | imass2 5307 |
. . . . . . . . . . . . 13
        
           
      |
79 | 77, 78 | syl 16 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                           
      |
80 | | simprr 756 |
. . . . . . . . . . . 12
     TopOn 
TopOn 
             
                   
  |
81 | 79, 80 | sstrd 3469 |
. . . . . . . . . . 11
     TopOn 
TopOn 
             
                           
  |
82 | | eleq2 2525 |
. . . . . . . . . . . . 13
        

           |
83 | | imaeq2 5268 |
. . . . . . . . . . . . . 14
        
                  |
84 | 83 | sseq1d 3486 |
. . . . . . . . . . . . 13
        
                
   |
85 | 82, 84 | anbi12d 710 |
. . . . . . . . . . . 12
        
 
    
                    
    |
86 | 85 | rspcev 3173 |
. . . . . . . . . . 11
         

                      

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

   
   |
88 | 87 | rexlimdvaa 2942 |
. . . . . . . . 9
    TopOn 
TopOn              
 
               

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

        |
90 | 89 | ex 434 |
. . . . . . 7
   TopOn  TopOn 

                            
                

         |
91 | 90 | com23 78 |
. . . . . 6
   TopOn  TopOn 

                                              
   
     |
92 | 91 | exp4a 606 |
. . . . 5
   TopOn  TopOn 

                                             
   
      |
93 | 92 | ralimdv2 2899 |
. . . 4
   TopOn  TopOn 

      
                                      
   
     |
94 | 93 | imdistanda 693 |
. . 3
  TopOn  TopOn 

                                                  

   
      |
95 | | iscnp 18968 |
. . 3
  TopOn  TopOn 

                 


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

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

                                                |