Step | Hyp | Ref
| Expression |
1 | | elxp2 4874 |
. . 3
  
       |
2 | | pion 9335 |
. . . . . . . . 9
   |
3 | | suceloni 6672 |
. . . . . . . . 9

  |
4 | 2, 3 | syl 17 |
. . . . . . . 8

  |
5 | | vex 3060 |
. . . . . . . . 9
 |
6 | 5 | sucid 5525 |
. . . . . . . 8
 |
7 | | eleq2 2529 |
. . . . . . . . 9
     |
8 | 7 | rspcev 3162 |
. . . . . . . 8
  
   |
9 | 4, 6, 8 | sylancl 673 |
. . . . . . 7
    |
10 | 9 | adantl 472 |
. . . . . 6
 
 
  |
11 | | elequ2 1912 |
. . . . . . . . . . . . . 14
 
   |
12 | 11 | imbi1d 323 |
. . . . . . . . . . . . 13
       

        |
13 | 12 | 2ralbidv 2844 |
. . . . . . . . . . . 12
  
  
   
   
       |
14 | | opeq1 4180 |
. . . . . . . . . . . . . . . . . . 19
         |
15 | 14 | breq2d 4430 |
. . . . . . . . . . . . . . . . . 18
 
  
      |
16 | 15 | rexbidv 2913 |
. . . . . . . . . . . . . . . . 17
  
          |
17 | 16 | imbi2d 322 |
. . . . . . . . . . . . . . . 16
       

        |
18 | | elequ1 1905 |
. . . . . . . . . . . . . . . . 17
 
   |
19 | | opeq2 4181 |
. . . . . . . . . . . . . . . . . . 19
         |
20 | 19 | breq2d 4430 |
. . . . . . . . . . . . . . . . . 18
 
  
      |
21 | 20 | rexbidv 2913 |
. . . . . . . . . . . . . . . . 17
  
          |
22 | 18, 21 | imbi12d 326 |
. . . . . . . . . . . . . . . 16
       

        |
23 | 17, 22 | cbvral2v 3039 |
. . . . . . . . . . . . . . 15
 
 
      
 
      |
24 | 23 | ralbii 2831 |
. . . . . . . . . . . . . 14
 

 
      
 
       |
25 | | rexnal 2848 |
. . . . . . . . . . . . . . . . . . 19
       
    
               |
26 | | pm4.63 427 |
. . . . . . . . . . . . . . . . . . . . 21
         
           |
27 | | xp2nd 6856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
      |
28 | | ltpiord 9343 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
     
       |
29 | 28 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
       |
30 | 27, 29 | sylan2 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       
       |
31 | 30 | adantll 725 |
. . . . . . . . . . . . . . . . . . . . . 22
   
               |
32 | 31 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . . 21
   
       
    
            |
33 | 26, 32 | syl5bb 265 |
. . . . . . . . . . . . . . . . . . . 20
   
       
    
            |
34 | 33 | rexbidva 2910 |
. . . . . . . . . . . . . . . . . . 19
 
             
                |
35 | 25, 34 | syl5bbr 267 |
. . . . . . . . . . . . . . . . . 18
 
              
                |
36 | | xp1st 6855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
      |
37 | | elequ2 1912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
38 | 37 | imbi1d 323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       

        |
39 | 38 | 2ralbidv 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
  
   
   
       |
40 | 39 | rspccv 3159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

 
         
       |
41 | | opeq1 4180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
  
         |
42 | 41 | breq2d 4430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
              |
43 | 42 | rexbidv 2913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
 
              |
44 | 43 | imbi2d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
  
   

            |
45 | 44 | ralbidv 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
 
 
   
              |
46 | 45 | rspccv 3159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
 
            
           |
47 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    

       |
48 | | opeq2 4181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
      
             |
49 | 48 | breq2d 4430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
                      |
50 | 49 | rexbidv 2913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
 
                      |
51 | 47, 50 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
  
                             |
52 | 51 | rspccv 3159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
 
       
                          |
53 | 46, 52 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
 
                    
                |
54 | 40, 53 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

 
                     
                 |
55 | 54 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
   
                
                |
56 | 36, 55 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
   
              
                |
57 | 27, 56 | mpdi 43 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
   
         
               |
58 | 57 | 3imp 1208 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
                      |
59 | | 1st2nd2 6862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
             |
60 | 59 | breq2d 4430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  

              |
61 | 60 | rexbidv 2913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
 
               |
62 | 61 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
                         |
63 | 58, 62 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
           |
64 | | enqer 9377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
 
   |
66 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
   |
67 | | simpl 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
      |
68 | 65, 66, 67 | ertr4d 7413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
      |
69 | 68 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
       |
70 | 69 | reximdv 2873 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
       |
71 | 63, 70 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
                   |
72 | 71 | 3expia 1217 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
                     |
73 | 72 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . 22
           
       
             |
74 | 73 | impd 437 |
. . . . . . . . . . . . . . . . . . . . 21
           
                     |
75 | 74 | rexlimdva 2891 |
. . . . . . . . . . . . . . . . . . . 20
      
   
  
      
            |
76 | 75 | ex 440 |
. . . . . . . . . . . . . . . . . . 19
 

 
                            |
77 | 76 | com3r 82 |
. . . . . . . . . . . . . . . . . 18
        
      

  
   
         |
78 | 35, 77 | syl6bi 236 |
. . . . . . . . . . . . . . . . 17
 
                        
          |
79 | 78 | com13 83 |
. . . . . . . . . . . . . . . 16
 

 
                    

          |
80 | | mulcompi 9352 |
. . . . . . . . . . . . . . . . . . . 20
     |
81 | | enqbreq 9375 |
. . . . . . . . . . . . . . . . . . . . 21
      
      
       |
82 | 81 | anidms 655 |
. . . . . . . . . . . . . . . . . . . 20
 
               |
83 | 80, 82 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . 19
 
         |
84 | | opelxpi 4888 |
. . . . . . . . . . . . . . . . . . . 20
 
        |
85 | | breq1 4421 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
86 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
87 | 86, 5 | op2ndd 6836 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          |
88 | 87 | breq2d 4430 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
       |
89 | 88 | notbid 300 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
       |
90 | 85, 89 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
            |
91 | 90 | ralbidv 2839 |
. . . . . . . . . . . . . . . . . . . . . 22
         
         
      
        |
92 | | df-nq 9368 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
93 | 91, 92 | elrab2 3210 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
94 | 93 | simplbi2 635 |
. . . . . . . . . . . . . . . . . . . 20
                          |
95 | 84, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
                     |
96 | | breq1 4421 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
97 | 96 | rspcev 3162 |
. . . . . . . . . . . . . . . . . . . 20
                  |
98 | 97 | expcom 441 |
. . . . . . . . . . . . . . . . . . 19
                  |
99 | 83, 95, 98 | sylsyld 58 |
. . . . . . . . . . . . . . . . . 18
 
               
      |
100 | 99 | com12 32 |
. . . . . . . . . . . . . . . . 17
 
      
               |
101 | 100 | a1dd 47 |
. . . . . . . . . . . . . . . 16
 
      
                 |
102 | 79, 101 | pm2.61d2 165 |
. . . . . . . . . . . . . . 15
 

 
      

         |
103 | 102 | ralrimivv 2820 |
. . . . . . . . . . . . . 14
 

 
        
      |
104 | 24, 103 | sylbir 218 |
. . . . . . . . . . . . 13
 

 
        
      |
105 | 104 | a1i 11 |
. . . . . . . . . . . 12
  

  
   
  
        |
106 | 13, 105 | tfis2 6715 |
. . . . . . . . . . 11
   
       |
107 | | rsp 2766 |
. . . . . . . . . . 11
 
 
                |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
    
       |
109 | | rsp 2766 |
. . . . . . . . . 10
 
 
   
  
       |
110 | 108, 109 | syl6 34 |
. . . . . . . . 9
    
        |
111 | 110 | impd 437 |
. . . . . . . 8
             |
112 | 111 | com12 32 |
. . . . . . 7
 
           |
113 | 112 | rexlimdv 2889 |
. . . . . 6
 
          |
114 | 10, 113 | mpd 15 |
. . . . 5
 
       |
115 | | breq2 4422 |
. . . . . 6
           |
116 | 115 | rexbidv 2913 |
. . . . 5
             |
117 | 114, 116 | syl5ibrcom 230 |
. . . 4
 
         |
118 | 117 | rexlimivv 2896 |
. . 3
  
      |
119 | 1, 118 | sylbi 200 |
. 2
  
   |
120 | | breq2 4422 |
. . . . . 6
 
   |
121 | | breq2 4422 |
. . . . . 6
 
   |
122 | 120, 121 | anbi12d 722 |
. . . . 5
  
      |
123 | 122 | imbi1d 323 |
. . . 4
    

 

    |
124 | 123 | 2ralbidv 2844 |
. . 3
  
  


         |
125 | 64 | a1i 11 |
. . . . . 6
       |
126 | | simpl 463 |
. . . . . 6
     |
127 | | simpr 467 |
. . . . . 6
  
  |
128 | 125, 126,
127 | ertr4d 7413 |
. . . . 5
     |
129 | | mulcompi 9352 |
. . . . . . . . . . 11
                     |
130 | | elpqn 9381 |
. . . . . . . . . . . . . . 15
     |
131 | | breq1 4421 |
. . . . . . . . . . . . . . . . . . 19
 
   |
132 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . 21
           |
133 | 132 | breq2d 4430 |
. . . . . . . . . . . . . . . . . . . 20
                     |
134 | 133 | notbid 300 |
. . . . . . . . . . . . . . . . . . 19
         
           |
135 | 131, 134 | imbi12d 326 |
. . . . . . . . . . . . . . . . . 18
           

            |
136 | 135 | ralbidv 2839 |
. . . . . . . . . . . . . . . . 17
  
            
    
            |
137 | 136, 92 | elrab2 3210 |
. . . . . . . . . . . . . . . 16

       
            |
138 | 137 | simprbi 470 |
. . . . . . . . . . . . . . 15
     
           |
139 | | breq2 4422 |
. . . . . . . . . . . . . . . . 17
 
   |
140 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . 19
           |
141 | 140 | breq1d 4428 |
. . . . . . . . . . . . . . . . . 18
                     |
142 | 141 | notbid 300 |
. . . . . . . . . . . . . . . . 17
         
           |
143 | 139, 142 | imbi12d 326 |
. . . . . . . . . . . . . . . 16
           

            |
144 | 143 | rspcva 3160 |
. . . . . . . . . . . . . . 15
    
                          |
145 | 130, 138,
144 | syl2anr 485 |
. . . . . . . . . . . . . 14
 
             |
146 | 145 | imp 435 |
. . . . . . . . . . . . 13
   

          |
147 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
   |
148 | | id 22 |
. . . . . . . . . . . . . . . . . 18
   |
149 | 147, 148 | ersym 7406 |
. . . . . . . . . . . . . . . . 17
   |
150 | | elpqn 9381 |
. . . . . . . . . . . . . . . . . 18
     |
151 | 92 | rabeq2i 3054 |
. . . . . . . . . . . . . . . . . . 19

       
            |
152 | 151 | simprbi 470 |
. . . . . . . . . . . . . . . . . 18
     
           |
153 | | breq2 4422 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
154 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
155 | 154 | breq1d 4428 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
156 | 155 | notbid 300 |
. . . . . . . . . . . . . . . . . . . 20
         
           |
157 | 153, 156 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . 19
           

            |
158 | 157 | rspcva 3160 |
. . . . . . . . . . . . . . . . . 18
    
                          |
159 | 150, 152,
158 | syl2an 484 |
. . . . . . . . . . . . . . . . 17
 
             |
160 | 149, 159 | syl5 33 |
. . . . . . . . . . . . . . . 16
 
             |
161 | 160 | imp 435 |
. . . . . . . . . . . . . . 15
   

          |
162 | | xp2nd 6856 |
. . . . . . . . . . . . . . . . . 18
  
      |
163 | 150, 162 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
164 | 163 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
   

      |
165 | | xp2nd 6856 |
. . . . . . . . . . . . . . . . . 18
  
      |
166 | 130, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
167 | 166 | ad2antlr 738 |
. . . . . . . . . . . . . . . 16
   

      |
168 | | ltsopi 9344 |
. . . . . . . . . . . . . . . . . . 19
 |
169 | | sotric 4803 |
. . . . . . . . . . . . . . . . . . 19
                    
                     |
170 | 168, 169 | mpan 681 |
. . . . . . . . . . . . . . . . . 18
                   
                     |
171 | 170 | notbid 300 |
. . . . . . . . . . . . . . . . 17
                   
                     |
172 | | notnot 297 |
. . . . . . . . . . . . . . . . 17
                  
                    |
173 | 171, 172 | syl6bbr 271 |
. . . . . . . . . . . . . . . 16
                   
                     |
174 | 164, 167,
173 | syl2anc 671 |
. . . . . . . . . . . . . . 15
   

                              |
175 | 161, 174 | mpbid 215 |
. . . . . . . . . . . . . 14
   

                    |
176 | 175 | ord 383 |
. . . . . . . . . . . . 13
   

        
           |
177 | 146, 176 | mt3d 130 |
. . . . . . . . . . . 12
   

          |
178 | 177 | oveq2d 6336 |
. . . . . . . . . . 11
   

                      |
179 | 129, 178 | syl5eq 2508 |
. . . . . . . . . 10
   

                      |
180 | | 1st2nd2 6862 |
. . . . . . . . . . . . . 14
  
             |
181 | | 1st2nd2 6862 |
. . . . . . . . . . . . . 14
  
             |
182 | 180, 181 | breqan12d 4434 |
. . . . . . . . . . . . 13
       
                         |
183 | | xp1st 6855 |
. . . . . . . . . . . . . . 15
  
      |
184 | 183, 162 | jca 539 |
. . . . . . . . . . . . . 14
  
            |
185 | | xp1st 6855 |
. . . . . . . . . . . . . . 15
  
      |
186 | 185, 165 | jca 539 |
. . . . . . . . . . . . . 14
  
            |
187 | | enqbreq 9375 |
. . . . . . . . . . . . . 14
                                  
                                  |
188 | 184, 186,
187 | syl2an 484 |
. . . . . . . . . . . . 13
                                                     |
189 | 182, 188 | bitrd 261 |
. . . . . . . . . . . 12
       
                       |
190 | 150, 130,
189 | syl2an 484 |
. . . . . . . . . . 11
 
                         |
191 | 190 | biimpa 491 |
. . . . . . . . . 10
   

                      |
192 | 179, 191 | eqtrd 2496 |
. . . . . . . . 9
   

                      |
193 | 150 | ad2antrr 737 |
. . . . . . . . . 10
   


   |
194 | | mulcanpi 9356 |
. . . . . . . . . . 11
                                           |
195 | 162, 183,
194 | syl2anc 671 |
. . . . . . . . . 10
  
                    
           |
196 | 193, 195 | syl 17 |
. . . . . . . . 9
   

                    
           |
197 | 192, 196 | mpbid 215 |
. . . . . . . 8
   

          |
198 | 197, 177 | opeq12d 4188 |
. . . . . . 7
   

          
             |
199 | 193, 180 | syl 17 |
. . . . . . 7
   

             |
200 | 130 | ad2antlr 738 |
. . . . . . . 8
   


   |
201 | 200, 181 | syl 17 |
. . . . . . 7
   

             |
202 | 198, 199,
201 | 3eqtr4d 2506 |
. . . . . 6
   

  |
203 | 202 | ex 440 |
. . . . 5
 
     |
204 | 128, 203 | syl5 33 |
. . . 4
 
   
   |
205 | 204 | rgen2a 2827 |
. . 3
       |
206 | 124, 205 | vtoclg 3119 |
. 2
  
        |
207 | | breq1 4421 |
. . 3
 
   |
208 | 207 | reu4 3244 |
. 2
 
     
     |
209 | 119, 206,
208 | sylanbrc 675 |
1
  
   |