Step | Hyp | Ref
| Expression |
1 | | neibastop1.1 |
. . . . . . . . 9
   |
2 | | neibastop1.2 |
. . . . . . . . 9
             |
3 | | neibastop1.3 |
. . . . . . . . 9
 

   
          
 
    |
4 | | neibastop1.4 |
. . . . . . . . 9
 

         |
5 | 1, 2, 3, 4 | neibastop1 31008 |
. . . . . . . 8
 TopOn    |
6 | | topontop 19934 |
. . . . . . . 8
 TopOn 
  |
7 | 5, 6 | syl 17 |
. . . . . . 7
   |
8 | 7 | adantr 467 |
. . . . . 6
 
   |
9 | | eqid 2450 |
. . . . . . 7
   |
10 | 9 | neii1 20115 |
. . . . . 6
 
              |
11 | 8, 10 | sylan 474 |
. . . . 5
                  |
12 | | toponuni 19935 |
. . . . . . 7
 TopOn 
   |
13 | 5, 12 | syl 17 |
. . . . . 6
    |
14 | 13 | ad2antrr 731 |
. . . . 5
              
   |
15 | 11, 14 | sseqtr4d 3468 |
. . . 4
                 |
16 | | neii2 20117 |
. . . . . 6
 
                  |
17 | 8, 16 | sylan 474 |
. . . . 5
               
      |
18 | | pweq 3953 |
. . . . . . . . . . 11
 
   |
19 | 18 | ineq2d 3633 |
. . . . . . . . . 10
     
           |
20 | 19 | neeq1d 2682 |
. . . . . . . . 9
        
          |
21 | 20 | raleqbi1dv 2994 |
. . . . . . . 8
  
      

          |
22 | 21, 4 | elrab2 3197 |
. . . . . . 7

  
    
     |
23 | | simprrr 774 |
. . . . . . . . . . . . 13
   

                     |
24 | | sspwb 4648 |
. . . . . . . . . . . . 13

    |
25 | 23, 24 | sylib 200 |
. . . . . . . . . . . 12
   

                       |
26 | | sslin 3657 |
. . . . . . . . . . . 12
 
            
    |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
   

                                   |
28 | | simprrl 773 |
. . . . . . . . . . . . 13
   

                       |
29 | | snssg 4104 |
. . . . . . . . . . . . . 14
 
     |
30 | 29 | ad3antlr 736 |
. . . . . . . . . . . . 13
   

                         |
31 | 28, 30 | mpbird 236 |
. . . . . . . . . . . 12
   

                     |
32 | | fveq2 5863 |
. . . . . . . . . . . . . . 15
           |
33 | 32 | ineq1d 3632 |
. . . . . . . . . . . . . 14
     
           |
34 | 33 | neeq1d 2682 |
. . . . . . . . . . . . 13
        
          |
35 | 34 | rspcv 3145 |
. . . . . . . . . . . 12
  
           
     |
36 | 31, 35 | syl 17 |
. . . . . . . . . . 11
   

                    
                 |
37 | | ssn0 3766 |
. . . . . . . . . . 11
             
 
       
         |
38 | 27, 36, 37 | syl6an 548 |
. . . . . . . . . 10
   

                    
                 |
39 | 38 | expr 619 |
. . . . . . . . 9
   

          
 
   
  
                  |
40 | 39 | com23 81 |
. . . . . . . 8
   

          
 
 
    
           
      |
41 | 40 | expimpd 607 |
. . . . . . 7
                  
    
            
      |
42 | 22, 41 | syl5bi 221 |
. . . . . 6
                         
      |
43 | 42 | rexlimdv 2876 |
. . . . 5
                         
     |
44 | 17, 43 | mpd 15 |
. . . 4
                        |
45 | 15, 44 | jca 535 |
. . 3
                          |
46 | 45 | ex 436 |
. 2
 
 
                      |
47 | | n0 3740 |
. . . 4
     
 
          |
48 | | elin 3616 |
. . . . . 6
       
    
    |
49 | | simprl 763 |
. . . . . . . . 9
         
      |
50 | 13 | ad2antrr 731 |
. . . . . . . . 9
         
   
   |
51 | 49, 50 | sseqtrd 3467 |
. . . . . . . 8
         
       |
52 | 1 | ad2antrr 731 |
. . . . . . . . 9
         
   
  |
53 | 2 | ad2antrr 731 |
. . . . . . . . 9
         
                |
54 | | simpll 759 |
. . . . . . . . . 10
         
      |
55 | 54, 3 | sylan 474 |
. . . . . . . . 9
   
               
          
 
    |
56 | | neibastop1.5 |
. . . . . . . . . 10
 

     
  |
57 | 54, 56 | sylan 474 |
. . . . . . . . 9
   
                 
  |
58 | | neibastop1.6 |
. . . . . . . . . 10
 

      
     
         |
59 | 54, 58 | sylan 474 |
. . . . . . . . 9
   
                  
     
         |
60 | | simplr 761 |
. . . . . . . . 9
         
   
  |
61 | | simprrl 773 |
. . . . . . . . 9
         
          |
62 | | simprrr 774 |
. . . . . . . . . 10
         
       |
63 | 62 | elpwid 3960 |
. . . . . . . . 9
         
   
  |
64 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
65 | 64 | ineq1d 3632 |
. . . . . . . . . . . . . . 15
     
           |
66 | 65 | cbviunv 4316 |
. . . . . . . . . . . . . 14

                |
67 | | pweq 3953 |
. . . . . . . . . . . . . . . 16
 
   |
68 | 67 | ineq2d 3633 |
. . . . . . . . . . . . . . 15
     
           |
69 | 68 | iuneq2d 4304 |
. . . . . . . . . . . . . 14
 
                 |
70 | 66, 69 | syl5eq 2496 |
. . . . . . . . . . . . 13
 
                 |
71 | 70 | cbviunv 4316 |
. . . . . . . . . . . 12

                  |
72 | 71 | mpteq2i 4485 |
. . . . . . . . . . 11
 
                     |
73 | | rdgeq1 7126 |
. . . . . . . . . . 11
  

    
    

    
                       

    
         |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . 10
    
    
          
              |
75 | 74 | reseq1i 5100 |
. . . . . . . . 9
                       
            
  |
76 | | pweq 3953 |
. . . . . . . . . . . . . 14
 
   |
77 | 76 | ineq2d 3633 |
. . . . . . . . . . . . 13
     
           |
78 | 77 | neeq1d 2682 |
. . . . . . . . . . . 12
        
          |
79 | 78 | cbvrexv 3019 |
. . . . . . . . . . 11
       
            
        
                               |
80 | | fveq2 5863 |
. . . . . . . . . . . . . 14
           |
81 | 80 | ineq1d 3632 |
. . . . . . . . . . . . 13
     
           |
82 | 81 | neeq1d 2682 |
. . . . . . . . . . . 12
        
          |
83 | 82 | rexbidv 2900 |
. . . . . . . . . . 11
  
     
            
        
                                |
84 | 79, 83 | syl5bb 261 |
. . . . . . . . . 10
  
     
            
        
                                |
85 | 84 | cbvrabv 3043 |
. . . . . . . . 9


                              
     
            
           |
86 | 52, 53, 55, 4, 57, 59, 60, 49, 61, 63, 75, 85 | neibastop2lem 31009 |
. . . . . . . 8
         
    

   |
87 | 7 | ad2antrr 731 |
. . . . . . . . 9
         
   
  |
88 | 60, 50 | eleqtrd 2530 |
. . . . . . . . 9
         
   
   |
89 | 9 | isneip 20114 |
. . . . . . . . 9
 
            
  

     |
90 | 87, 88, 89 | syl2anc 666 |
. . . . . . . 8
         
              
  

     |
91 | 51, 86, 90 | mpbir2and 932 |
. . . . . . 7
         
   
            |
92 | 91 | expr 619 |
. . . . . 6
                          |
93 | 48, 92 | syl5bi 221 |
. . . . 5
                          |
94 | 93 | exlimdv 1778 |
. . . 4
      
                    |
95 | 47, 94 | syl5bi 221 |
. . 3
                          |
96 | 95 | expimpd 607 |
. 2
 
          
             |
97 | 46, 96 | impbid 194 |
1
 
 
         
            |