Step | Hyp | Ref
| Expression |
1 | | neibastop2.s |
. . . . 5
             |
2 | | ssrab2 3544 |
. . . . 5
 
           |
3 | 1, 2 | eqsstri 3493 |
. . . 4
 |
4 | | neibastop1.1 |
. . . . 5
   |
5 | | elpw2g 4562 |
. . . . 5
 
    |
6 | 4, 5 | syl 16 |
. . . 4
  
   |
7 | 3, 6 | mpbiri 233 |
. . 3
    |
8 | | fveq2 5798 |
. . . . . . . . 9
           |
9 | 8 | ineq1d 3658 |
. . . . . . . 8
     
           |
10 | 9 | neeq1d 2728 |
. . . . . . 7
        
          |
11 | 10 | rexbidv 2864 |
. . . . . 6
  
        
       
     |
12 | 11, 1 | elrab2 3224 |
. . . . 5


       
     |
13 | | frfnom 6999 |
. . . . . . . . . 10
                    |
14 | | neibastop2.g |
. . . . . . . . . . 11
    

    
         |
15 | 14 | fneq1i 5612 |
. . . . . . . . . 10

                     |
16 | 13, 15 | mpbir 209 |
. . . . . . . . 9
 |
17 | | fnunirn 6078 |
. . . . . . . . 9
   
       |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
         |
19 | | n0 3753 |
. . . . . . . . . 10
     
 
          |
20 | | inss1 3677 |
. . . . . . . . . . . . . . . 16
            |
21 | 20 | sseli 3459 |
. . . . . . . . . . . . . . 15
              |
22 | | neibastop1.6 |
. . . . . . . . . . . . . . . 16
 

      
     
         |
23 | 22 | anassrs 648 |
. . . . . . . . . . . . . . 15
                         |
24 | 21, 23 | sylan2 474 |
. . . . . . . . . . . . . 14
            
     
         |
25 | 24 | adantrl 715 |
. . . . . . . . . . . . 13
               
    
     
         |
26 | | simprl 755 |
. . . . . . . . . . . . . 14
   
  
                  

               |
27 | | fvssunirn 5821 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      |
28 | | neibastop1.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
29 | | frn 5672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
30 | 28, 29 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
31 | 30 | difss2d 3593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
32 | | sspwuni 4363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  
   |
33 | 31, 32 | sylib 196 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
34 | 33 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               
        |
35 | 27, 34 | syl5ss 3474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               
       
   |
36 | 35 | sselda 3463 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  
                  
   |
37 | 36 | elpwid 3977 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  
                  
  |
38 | 37 | sselda 3463 |
. . . . . . . . . . . . . . . . . . . . 21
                              |
39 | 38 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
                                
      |
40 | | simprlr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               
          |
41 | | rspe 2893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
        
         |
42 | 41 | ad2ant2l 745 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               
    
         |
43 | | eliun 4282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        

         |
44 | | pweq 3970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
   |
45 | 44 | ineq2d 3659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
           |
46 | 45 | eleq2d 2524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
47 | 46 | rexbidv 2864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
      

          |
48 | 43, 47 | syl5bb 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
      

          |
49 | 48 | rspcev 3177 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                     
         |
50 | 40, 42, 49 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               
    
     
         |
51 | | eliun 4282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              
      
    
    |
52 | 50, 51 | sylibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               
                    |
53 | | simpll 753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               
      |
54 | | simprll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               
      |
55 | | fvssunirn 5821 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      |
56 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36

          |
57 | 14 | fveq1i 5799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
         

    
            |
58 | | snex 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
 |
59 | | fr0g 7000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
         
    
               |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     
                    |
61 | 57, 60 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       |
62 | 56, 61 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

        |
63 | 62 | sseq1d 3490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

     
      |
64 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           |
65 | 64 | sseq1d 3490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
         |
66 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       
   |
67 | 66 | sseq1d 3490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
               |
68 | | neibastop2.f |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       |
69 | | pwidg 3980 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
        |
70 | 68, 69 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    |
71 | 70 | snssd 4125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      |
72 | | simprl 755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
          |
73 | 68 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
       
      |
74 | | pwexg 4583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     
  |
75 | 73, 74 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
        
  |
76 | | inss2 3678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
         |
77 | | elpwi 3976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 
  |
78 | 77 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 
    |
79 | | sspwb 4648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46

    |
80 | 78, 79 | sylib 196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 
      |
81 | 76, 80 | syl5ss 3474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
      
 
   |
82 | 81 | ralrimivw 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 
  
          |
83 | | iunss 4318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 
    
 
      
 
   |
84 | 82, 83 | sylibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 
  
          |
85 | 84 | ralrimiva 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
              |
86 | | ssralv 3523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
       
                            |
87 | 86 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
           
       
                  |
88 | 85, 87 | mpan9 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
        
     
          |
89 | | iunss 4318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
     
       
                 |
90 | 88, 89 | sylibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
        
     
          |
91 | 75, 90 | ssexd 4546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
        
     
         |
92 | | iuneq1 4291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
                   |
93 | | iuneq1 4291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     
                        |
94 | 14, 92, 93 | frsucmpt2 7004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
        
    
       
     
         |
95 | 72, 91, 94 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
            
     
         |
96 | 95, 90 | eqsstrd 3497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
               |
97 | 96 | expr 615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 

              |
98 | 97 | expcom 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       
  
      |
99 | 63, 65, 67, 71, 98 | finds2 6613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
          |
100 | | fvex 5808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
101 | 100 | elpw 3973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
              |
102 | 99, 101 | syl6ibr 227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
103 | 102 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
104 | 103 | ralrimiv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          |
105 | | ffnfv 5977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                  |
106 | 16, 105 | mpbiran 909 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                |
107 | 104, 106 | sylibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
108 | | frn 5672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
    |
109 | 107, 108 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
110 | | sspwuni 4363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  
   |
111 | 109, 110 | sylib 196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
112 | 111 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               
        |
113 | 55, 112 | syl5ss 3474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               
       
   |
114 | 53, 54, 113, 95 | syl12anc 1217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               
        
     
         |
115 | 52, 114 | eleqtrrd 2545 |
. . . . . . . . . . . . . . . . . . . . . . 23
               
      
   |
116 | | peano2 6605 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
117 | 54, 116 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               
   
  |
118 | | fnfvelrn 5948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
119 | 16, 117, 118 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . . . . 23
               
          |
120 | | elunii 4203 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
     
   |
121 | 115, 119,
120 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . . 22
               
       |
122 | 121 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
                                
       |
123 | | simprr 756 |
. . . . . . . . . . . . . . . . . . . . 21
                                
             |
124 | | pweq 3970 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
125 | 124 | ineq2d 3659 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
           |
126 | 125 | neeq1d 2728 |
. . . . . . . . . . . . . . . . . . . . . 22
        
          |
127 | 126 | rspcev 3177 |
. . . . . . . . . . . . . . . . . . . . 21
          
       
    |
128 | 122, 123,
127 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . 20
                                
                |
129 | 1 | rabeq2i 3073 |
. . . . . . . . . . . . . . . . . . . 20


       
     |
130 | 39, 128, 129 | sylanbrc 664 |
. . . . . . . . . . . . . . . . . . 19
                                
      |
131 | 130 | expr 615 |
. . . . . . . . . . . . . . . . . 18
                                       |
132 | 131 | ralimdva 2831 |
. . . . . . . . . . . . . . . . 17
   
  
                  
 
    
  
   |
133 | 132 | impr 619 |
. . . . . . . . . . . . . . . 16
   
  
                  

         
  |
134 | | dfss3 3453 |
. . . . . . . . . . . . . . . 16


  |
135 | 133, 134 | sylibr 212 |
. . . . . . . . . . . . . . 15
   
  
                  

           |
136 | | selpw 3974 |
. . . . . . . . . . . . . . 15
 
  |
137 | 135, 136 | sylibr 212 |
. . . . . . . . . . . . . 14
   
  
                  

            |
138 | | inelcm 3840 |
. . . . . . . . . . . . . 14
     
 
         |
139 | 26, 137, 138 | syl2anc 661 |
. . . . . . . . . . . . 13
   
  
                  

             
    |
140 | 25, 139 | rexlimddv 2949 |
. . . . . . . . . . . 12
               
             |
141 | 140 | expr 615 |
. . . . . . . . . . 11
    
                  
     |
142 | 141 | exlimdv 1691 |
. . . . . . . . . 10
    
                         |
143 | 19, 142 | syl5bi 217 |
. . . . . . . . 9
    
             
          |
144 | 143 | rexlimdvaa 2946 |
. . . . . . . 8
 
  
                
      |
145 | 18, 144 | syl5bi 217 |
. . . . . . 7
 
          
           |
146 | 145 | rexlimdv 2944 |
. . . . . 6
 
  
             
     |
147 | 146 | expimpd 603 |
. . . . 5
          
             |
148 | 12, 147 | syl5bi 217 |
. . . 4
            |
149 | 148 | ralrimiv 2827 |
. . 3
           |
150 | | pweq 3970 |
. . . . . . 7
 
   |
151 | 150 | ineq2d 3659 |
. . . . . 6
     
           |
152 | 151 | neeq1d 2728 |
. . . . 5
        
          |
153 | 152 | raleqbi1dv 3029 |
. . . 4
  
      

          |
154 | | neibastop1.4 |
. . . 4
 

         |
155 | 153, 154 | elrab2 3224 |
. . 3

  
    
     |
156 | 7, 149, 155 | sylanbrc 664 |
. 2
   |
157 | | neibastop2.p |
. . 3
   |
158 | | snidg 4010 |
. . . . . 6
         |
159 | 68, 158 | syl 16 |
. . . . 5
     |
160 | | peano1 6604 |
. . . . . . 7
 |
161 | | fnfvelrn 5948 |
. . . . . . 7
         |
162 | 16, 160, 161 | mp2an 672 |
. . . . . 6
     |
163 | 61, 162 | eqeltrri 2539 |
. . . . 5
 
 |
164 | | elunii 4203 |
. . . . 5
      
   |
165 | 159, 163,
164 | sylancl 662 |
. . . 4
    |
166 | | inelcm 3840 |
. . . . 5
     
 
         |
167 | 68, 70, 166 | syl2anc 661 |
. . . 4
          |
168 | | pweq 3970 |
. . . . . . 7
 
   |
169 | 168 | ineq2d 3659 |
. . . . . 6
     
           |
170 | 169 | neeq1d 2728 |
. . . . 5
        
          |
171 | 170 | rspcev 3177 |
. . . 4
          
       
    |
172 | 165, 167,
171 | syl2anc 661 |
. . 3
             |
173 | | fveq2 5798 |
. . . . . . 7
           |
174 | 173 | ineq1d 3658 |
. . . . . 6
     
           |
175 | 174 | neeq1d 2728 |
. . . . 5
        
          |
176 | 175 | rexbidv 2864 |
. . . 4
  
        
       
     |
177 | 176, 1 | elrab2 3224 |
. . 3


       
     |
178 | 157, 172,
177 | sylanbrc 664 |
. 2
   |
179 | | eluni2 4202 |
. . . . . . 7
  
  |
180 | | eleq2 2527 |
. . . . . . . . . 10
     
       |
181 | 180 | rexrn 5953 |
. . . . . . . . 9
  
        |
182 | 16, 181 | ax-mp 5 |
. . . . . . . 8
 
       |
183 | 107 | adantr 465 |
. . . . . . . . . . . . . . . . 17
 
         |
184 | 183 | ffvelrnda 5951 |
. . . . . . . . . . . . . . . 16
             |
185 | 184 | elpwid 3977 |
. . . . . . . . . . . . . . 15
            |
186 | 185 | sselda 3463 |
. . . . . . . . . . . . . 14
   

     
   |
187 | 186 | adantrr 716 |
. . . . . . . . . . . . 13
   

     
            |
188 | 187 | elpwid 3977 |
. . . . . . . . . . . 12
   

     
           |
189 | | neibastop2.u |
. . . . . . . . . . . . 13

  |
190 | 189 | ad3antrrr 729 |
. . . . . . . . . . . 12
   

     
           |
191 | 188, 190 | sstrd 3473 |
. . . . . . . . . . 11
   

     
           |
192 | | n0 3753 |
. . . . . . . . . . . . 13
     
 
          |
193 | | elin 3646 |
. . . . . . . . . . . . . . 15
       
    
    |
194 | | simprrr 764 |
. . . . . . . . . . . . . . . . . 18
   

     
    
       |
195 | 194 | elpwid 3977 |
. . . . . . . . . . . . . . . . 17
   

     
    
      |
196 | | simpllr 758 |
. . . . . . . . . . . . . . . . . 18
   

     
    
      |
197 | | neibastop1.5 |
. . . . . . . . . . . . . . . . . . . . 21
 

     
  |
198 | 197 | expr 615 |
. . . . . . . . . . . . . . . . . . . 20
 
     
   |
199 | 198 | ralrimiva 2829 |
. . . . . . . . . . . . . . . . . . 19
          |
200 | 199 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
   

     
    
             |
201 | | simprrl 763 |
. . . . . . . . . . . . . . . . . 18
   

     
    
          |
202 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . 21
           |
203 | 202 | eleq2d 2524 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
204 | | elequ1 1761 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
205 | 203, 204 | imbi12d 320 |
. . . . . . . . . . . . . . . . . . 19
            
    |
206 | 205 | rspcv 3173 |
. . . . . . . . . . . . . . . . . 18
  
     
    
    |
207 | 196, 200,
201, 206 | syl3c 61 |
. . . . . . . . . . . . . . . . 17
   

     
    
      |
208 | 195, 207 | sseldd 3464 |
. . . . . . . . . . . . . . . 16
   

     
    
      |
209 | 208 | expr 615 |
. . . . . . . . . . . . . . 15
   

     
     
 
   |
210 | 193, 209 | syl5bi 217 |
. . . . . . . . . . . . . 14
   

     
           |
211 | 210 | exlimdv 1691 |
. . . . . . . . . . . . 13
   

     
 
    
 
   |
212 | 192, 211 | syl5bi 217 |
. . . . . . . . . . . 12
   

     
     
     |
213 | 212 | impr 619 |
. . . . . . . . . . 11
   

     
           |
214 | 191, 213 | sseldd 3464 |
. . . . . . . . . 10
   

     
           |
215 | 214 | exp32 605 |
. . . . . . . . 9
                      |
216 | 215 | rexlimdva 2945 |
. . . . . . . 8
 
  
                |
217 | 182, 216 | syl5bi 217 |
. . . . . . 7
 
  
            |
218 | 179, 217 | syl5bi 217 |
. . . . . 6
 
          
    |
219 | 218 | rexlimdv 2944 |
. . . . 5
 
  
            |
220 | 219 | 3impia 1185 |
. . . 4
 
 
     
     |
221 | 220 | rabssdv 3539 |
. . 3
            
  |
222 | 1, 221 | syl5eqss 3507 |
. 2

  |
223 | | eleq2 2527 |
. . . 4
 
   |
224 | | sseq1 3484 |
. . . 4
 
   |
225 | 223, 224 | anbi12d 710 |
. . 3
  
 
    |
226 | 225 | rspcev 3177 |
. 2
  
 


   |
227 | 156, 178,
222, 226 | syl12anc 1217 |
1
  
   |