Step | Hyp | Ref
| Expression |
1 | | neiptop.0 |
. . 3
         |
2 | 1 | feqmptd 5945 |
. 2
         |
3 | 1 | ffvelrnda 6050 |
. . . . . . . . . . . 12
 
         |
4 | 3 | adantr 471 |
. . . . . . . . . . 11
                 |
5 | 4 | elpwid 3973 |
. . . . . . . . . 10
                |
6 | | simpr 467 |
. . . . . . . . . 10
               |
7 | 5, 6 | sseldd 3445 |
. . . . . . . . 9
            |
8 | 7 | elpwid 3973 |
. . . . . . . 8
           |
9 | | neiptop.o |
. . . . . . . . . . 11
 

      |
10 | | neiptop.1 |
. . . . . . . . . . 11
   


           |
11 | | neiptop.2 |
. . . . . . . . . . 11
 
               |
12 | | neiptop.3 |
. . . . . . . . . . 11
           |
13 | | neiptop.4 |
. . . . . . . . . . 11
                      |
14 | | neiptop.5 |
. . . . . . . . . . 11
 
       |
15 | 9, 1, 10, 11, 12, 13, 14 | neiptopuni 20201 |
. . . . . . . . . 10
    |
16 | 15 | adantr 471 |
. . . . . . . . 9
 
    |
17 | 16 | adantr 471 |
. . . . . . . 8
            |
18 | 8, 17 | sseqtrd 3480 |
. . . . . . 7
            |
19 | | ssrab2 3526 |
. . . . . . . . . 10
       |
20 | 19 | a1i 11 |
. . . . . . . . 9
                 |
21 | | fveq2 5892 |
. . . . . . . . . . . . . 14
           |
22 | 21 | eleq2d 2525 |
. . . . . . . . . . . . 13
     
       |
23 | 22 | elrab 3208 |
. . . . . . . . . . . 12
      

       |
24 | | simp-5l 783 |
. . . . . . . . . . . . . 14
     
      
                 
  |
25 | | simpr1l 1071 |
. . . . . . . . . . . . . . 15
   

    
 
    
    
         |
26 | 25 | 3anassrs 1240 |
. . . . . . . . . . . . . 14
     
      
                 
  |
27 | | simpr 467 |
. . . . . . . . . . . . . 14
     
      
                 
        |
28 | | simplr 767 |
. . . . . . . . . . . . . 14
     
      
                 
      |
29 | | sseq1 3465 |
. . . . . . . . . . . . . . . . . . . 20
 

    
         |
30 | 29 | 3anbi2d 1353 |
. . . . . . . . . . . . . . . . . . 19
   

            
  
                |
31 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . 19
     
       |
32 | 30, 31 | anbi12d 722 |
. . . . . . . . . . . . . . . . . 18
                  
    
  
 
           
        |
33 | 32 | imbi1d 323 |
. . . . . . . . . . . . . . . . 17
     
 
           
    

               
           
    

             |
34 | | simpl1l 1065 |
. . . . . . . . . . . . . . . . . 18
   

            
       |
35 | 9, 1, 10, 11, 12, 13, 14 | neiptoptop 20202 |
. . . . . . . . . . . . . . . . . . . . 21
   |
36 | | uniexg 6620 |
. . . . . . . . . . . . . . . . . . . . 21
    |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
    |
38 | 15, 37 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . 19
   |
39 | | rabexg 4570 |
. . . . . . . . . . . . . . . . . . 19
         |
40 | | sseq2 3466 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
         |
41 | | sseq1 3465 |
. . . . . . . . . . . . . . . . . . . . . . 23
       

        |
42 | 40, 41 | 3anbi23d 1351 |
. . . . . . . . . . . . . . . . . . . . . 22
         


  
                |
43 | 42 | anbi1d 716 |
. . . . . . . . . . . . . . . . . . . . 21
           
        
 
           
        |
44 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . 21
           

            |
45 | 43, 44 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . 20
           
           
   

            
     
    
        |
46 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
47 | 46 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

     |
48 | 47 | 3anbi1d 1352 |
. . . . . . . . . . . . . . . . . . . . . . 23
   


  
    |
49 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
50 | 49 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
       |
51 | 48, 50 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . . 22
     
        
          |
52 | 49 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
53 | 51, 52 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . 21
     
           
   


             |
54 | 53, 10 | chvarv 2118 |
. . . . . . . . . . . . . . . . . . . 20
   


           |
55 | 45, 54 | vtoclg 3119 |
. . . . . . . . . . . . . . . . . . 19
                        
     
    
       |
56 | 38, 39, 55 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
    
 
           
    

            |
57 | 34, 56 | mpcom 37 |
. . . . . . . . . . . . . . . . 17
   

            
     
    
      |
58 | 33, 57 | chvarv 2118 |
. . . . . . . . . . . . . . . 16
   

            
     
    
      |
59 | 58 | 3an1rs 1229 |
. . . . . . . . . . . . . . 15
   

     
            
    
      |
60 | 19, 59 | mpan2 682 |
. . . . . . . . . . . . . 14
    
         

           |
61 | 24, 26, 27, 28, 60 | syl211anc 1282 |
. . . . . . . . . . . . 13
     
      
                 

           |
62 | | simplll 773 |
. . . . . . . . . . . . . 14
   

    

        |
63 | | simprl 769 |
. . . . . . . . . . . . . 14
   

    

        |
64 | | simprr 771 |
. . . . . . . . . . . . . 14
   

    

            |
65 | 49 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
66 | 47, 65 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . 19
   

                |
67 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
68 | 67 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
69 | 68 | cbvralv 3031 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
  
   

       |
71 | 49, 70 | rexeqbidv 3014 |
. . . . . . . . . . . . . . . . . . 19
  
     
   
              |
72 | 66, 71 | imbi12d 326 |
. . . . . . . . . . . . . . . . . 18
          
              
                     |
73 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
74 | 73 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . 20
   

                |
75 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
76 | 75 | rexralbidv 2921 |
. . . . . . . . . . . . . . . . . . . 20
  
     
   
              |
77 | 74, 76 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . 19
          
              
                     |
78 | 77, 13 | chvarv 2118 |
. . . . . . . . . . . . . . . . . 18
                      |
79 | 72, 78 | chvarv 2118 |
. . . . . . . . . . . . . . . . 17
                      |
80 | 1 | ffvelrnda 6050 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
         |
81 | 80 | elpwid 3973 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
        |
82 | 81 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            |
83 | 82 | elpwid 3973 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
84 | 83 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . 22
   

    
   |
85 | 84 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
         |
86 | 85 | ancrd 561 |
. . . . . . . . . . . . . . . . . . . 20
   

    
      
        |
87 | 86 | ralimdva 2808 |
. . . . . . . . . . . . . . . . . . 19
          
    

        |
88 | 87 | reximdva 2874 |
. . . . . . . . . . . . . . . . . 18
 
  
     
    
     

        |
89 | 88 | adantr 471 |
. . . . . . . . . . . . . . . . 17
          
     
    
     

        |
90 | 79, 89 | mpd 15 |
. . . . . . . . . . . . . . . 16
                        |
91 | 68 | elrab 3208 |
. . . . . . . . . . . . . . . . . 18
      

       |
92 | 91 | ralbii 2831 |
. . . . . . . . . . . . . . . . 17
 

      
       |
93 | 92 | rexbii 2901 |
. . . . . . . . . . . . . . . 16
       

            
       |
94 | 90, 93 | sylibr 217 |
. . . . . . . . . . . . . . 15
                        |
95 | | dfss3 3434 |
. . . . . . . . . . . . . . . . 17
      

        |
96 | 95 | biimpri 211 |
. . . . . . . . . . . . . . . 16
 

             |
97 | 96 | reximi 2867 |
. . . . . . . . . . . . . . 15
       

          

       |
98 | 94, 97 | syl 17 |
. . . . . . . . . . . . . 14
                       |
99 | 62, 63, 64, 98 | syl21anc 1275 |
. . . . . . . . . . . . 13
   

    

      
    

       |
100 | 61, 99 | r19.29a 2944 |
. . . . . . . . . . . 12
   

    

      
    
      |
101 | 23, 100 | sylan2b 482 |
. . . . . . . . . . 11
   

    
      

           |
102 | 101 | ralrimiva 2814 |
. . . . . . . . . 10
          
     
    
      |
103 | 49 | eleq2d 2525 |
. . . . . . . . . . 11
  
    
   

            |
104 | 103 | cbvralv 3031 |
. . . . . . . . . 10
 

               
                  |
105 | 102, 104 | sylibr 217 |
. . . . . . . . 9
          
     
    
      |
106 | 9 | neipeltop 20200 |
. . . . . . . . 9
      
       

                  |
107 | 20, 105, 106 | sylanbrc 675 |
. . . . . . . 8
                 |
108 | | simpr 467 |
. . . . . . . . . 10
 
   |
109 | 108 | anim1i 576 |
. . . . . . . . 9
         
       |
110 | | fveq2 5892 |
. . . . . . . . . . 11
           |
111 | 110 | eleq2d 2525 |
. . . . . . . . . 10
     
       |
112 | 111 | elrab 3208 |
. . . . . . . . 9
      

       |
113 | 109, 112 | sylibr 217 |
. . . . . . . 8
         
       |
114 | | nfv 1772 |
. . . . . . . . 9
   

      |
115 | | nfrab1 2983 |
. . . . . . . . 9
  
      |
116 | | nfcv 2603 |
. . . . . . . . 9
   |
117 | | rabid 2979 |
. . . . . . . . . 10
      

       |
118 | | simplll 773 |
. . . . . . . . . . . 12
   

    

        |
119 | | simprl 769 |
. . . . . . . . . . . 12
   

    

        |
120 | | simprr 771 |
. . . . . . . . . . . 12
   

    

            |
121 | | eleq1 2528 |
. . . . . . . . . . . . . . . 16
 
   |
122 | 121 | anbi2d 715 |
. . . . . . . . . . . . . . 15
  

     |
123 | | fveq2 5892 |
. . . . . . . . . . . . . . . 16
           |
124 | 123 | eleq2d 2525 |
. . . . . . . . . . . . . . 15
     
       |
125 | 122, 124 | anbi12d 722 |
. . . . . . . . . . . . . 14
   

                |
126 | | elequ1 1905 |
. . . . . . . . . . . . . 14
 
   |
127 | 125, 126 | imbi12d 326 |
. . . . . . . . . . . . 13
          

  
          |
128 | | elequ2 1912 |
. . . . . . . . . . . . . . 15
 
   |
129 | 74, 128 | imbi12d 326 |
. . . . . . . . . . . . . 14
          

  
          |
130 | 129, 12 | chvarv 2118 |
. . . . . . . . . . . . 13
           |
131 | 127, 130 | chvarv 2118 |
. . . . . . . . . . . 12
           |
132 | 118, 119,
120, 131 | syl21anc 1275 |
. . . . . . . . . . 11
   

    

        |
133 | 132 | ex 440 |
. . . . . . . . . 10
          
    
   |
134 | 117, 133 | syl5bi 225 |
. . . . . . . . 9
                   |
135 | 114, 115,
116, 134 | ssrd 3449 |
. . . . . . . 8
                 |
136 | | eleq2 2529 |
. . . . . . . . . 10
       
         |
137 | | sseq1 3465 |
. . . . . . . . . 10
       

        |
138 | 136, 137 | anbi12d 722 |
. . . . . . . . 9
           
               |
139 | 138 | rspcev 3162 |
. . . . . . . 8
  
    

               
   |
140 | 107, 113,
135, 139 | syl12anc 1274 |
. . . . . . 7
         

   |
141 | 18, 140 | jca 539 |
. . . . . 6
         
       |
142 | | nfv 1772 |
. . . . . . . 8
     |
143 | | nfv 1772 |
. . . . . . . . 9

  |
144 | | nfre1 2860 |
. . . . . . . . 9
   
  |
145 | 143, 144 | nfan 2022 |
. . . . . . . 8
     
   |
146 | 142, 145 | nfan 2022 |
. . . . . . 7
   
    
    |
147 | | simplll 773 |
. . . . . . . 8
        

             |
148 | | simpr 467 |
. . . . . . . 8
        

           |
149 | | simpr1l 1071 |
. . . . . . . . . 10
        
     
 
   |
150 | 149 | 3anassrs 1240 |
. . . . . . . . 9
        

            |
151 | 147, 16 | syl 17 |
. . . . . . . . 9
        

            |
152 | 150, 151 | sseqtr4d 3481 |
. . . . . . . 8
        

           |
153 | | simplr 767 |
. . . . . . . 8
        

               |
154 | | sseq1 3465 |
. . . . . . . . . . . 12
 
   |
155 | 154 | 3anbi2d 1353 |
. . . . . . . . . . 11
   


  
    |
156 | | eleq1 2528 |
. . . . . . . . . . 11
     
       |
157 | 155, 156 | anbi12d 722 |
. . . . . . . . . 10
     
        
          |
158 | 157 | imbi1d 323 |
. . . . . . . . 9
     
           
   


             |
159 | | sseq2 3466 |
. . . . . . . . . . . . 13
 
   |
160 | | sseq1 3465 |
. . . . . . . . . . . . 13
 
   |
161 | 159, 160 | 3anbi23d 1351 |
. . . . . . . . . . . 12
   


  
    |
162 | 161 | anbi1d 716 |
. . . . . . . . . . 11
     
        
          |
163 | | eleq1 2528 |
. . . . . . . . . . 11
     
       |
164 | 162, 163 | imbi12d 326 |
. . . . . . . . . 10
     
           
   


             |
165 | 164, 10 | chvarv 2118 |
. . . . . . . . 9
   


           |
166 | 158, 165 | chvarv 2118 |
. . . . . . . 8
   


           |
167 | 147, 148,
152, 153, 166 | syl31anc 1279 |
. . . . . . 7
        

               |
168 | 9 | neipeltop 20200 |
. . . . . . . . . . . . 13

 
       |
169 | 168 | simprbi 470 |
. . . . . . . . . . . 12
 
      |
170 | 169 | r19.21bi 2769 |
. . . . . . . . . . 11
 
       |
171 | 170 | anim1i 576 |
. . . . . . . . . 10
  

         |
172 | 171 | anasss 657 |
. . . . . . . . 9
  
 
    
   |
173 | 172 | reximi2 2866 |
. . . . . . . 8
    
    
  |
174 | 173 | ad2antll 740 |
. . . . . . 7
    
     
        |
175 | 146, 167,
174 | r19.29af 2942 |
. . . . . 6
    
     
      |
176 | 141, 175 | impbida 848 |
. . . . 5
 
     
  
      |
177 | 35 | adantr 471 |
. . . . . 6
 
   |
178 | 108, 16 | eleqtrd 2542 |
. . . . . 6
 
    |
179 | | eqid 2462 |
. . . . . . 7
   |
180 | 179 | isneip 20176 |
. . . . . 6
 
            
  
      |
181 | 177, 178,
180 | syl2anc 671 |
. . . . 5
 
              

     |
182 | 176, 181 | bitr4d 264 |
. . . 4
 
     
             |
183 | 182 | eqrdv 2460 |
. . 3
 
                 |
184 | 183 | mpteq2dva 4505 |
. 2
                     |
185 | 2, 184 | eqtrd 2496 |
1
               |