Step | Hyp | Ref
| Expression |
1 | | genpelvl.1 |
. . . . . . . . . 10
 
            
       
          
         |
2 | | genpelvl.2 |
. . . . . . . . . 10
 
       |
3 | 1, 2 | genpelvl 7499 |
. . . . . . . . 9
 
          
                  |
4 | | r2ex 2497 |
. . . . . . . . 9
                                       |
5 | 3, 4 | bitrdi 196 |
. . . . . . . 8
 
                                 |
6 | 5 | biimpa 296 |
. . . . . . 7
   
                  
            |
7 | 6 | adantrl 478 |
. . . . . 6
                        
            |
8 | | prop 7462 |
. . . . . . . . . . . . . . . 16
              |
9 | | prnmaxl 7475 |
. . . . . . . . . . . . . . . 16
                  
       |
10 | 8, 9 | sylan 283 |
. . . . . . . . . . . . . . 15
 
     
       |
11 | | prop 7462 |
. . . . . . . . . . . . . . . 16
              |
12 | | prnmaxl 7475 |
. . . . . . . . . . . . . . . 16
                  
       |
13 | 11, 12 | sylan 283 |
. . . . . . . . . . . . . . 15
 
     
       |
14 | 10, 13 | anim12i 338 |
. . . . . . . . . . . . . 14
        
                  
   |
15 | 14 | an4s 588 |
. . . . . . . . . . . . 13
                
    
         |
16 | | reeanv 2646 |
. . . . . . . . . . . . 13
             
             
   |
17 | 15, 16 | sylibr 134 |
. . . . . . . . . . . 12
                           
   |
18 | | genprndl.ord |
. . . . . . . . . . . . . . 15
 
 
           |
19 | | genprndl.com |
. . . . . . . . . . . . . . 15
 
           |
20 | 18, 19 | genplt2i 7497 |
. . . . . . . . . . . . . 14
 
    
      |
21 | 20 | reximi 2574 |
. . . . . . . . . . . . 13
       
                 |
22 | 21 | reximi 2574 |
. . . . . . . . . . . 12
             

                      |
23 | 17, 22 | syl 14 |
. . . . . . . . . . 11
                                     |
24 | 23 | adantrr 479 |
. . . . . . . . . 10
         
           
                     |
25 | | breq1 4003 |
. . . . . . . . . . . . . 14
         
           |
26 | 25 | biimprd 158 |
. . . . . . . . . . . . 13
         
           |
27 | 26 | reximdv 2578 |
. . . . . . . . . . . 12
      
            
             |
28 | 27 | reximdv 2578 |
. . . . . . . . . . 11
      
                  
                   |
29 | 28 | ad2antll 491 |
. . . . . . . . . 10
         
                                           
       |
30 | 24, 29 | mpd 13 |
. . . . . . . . 9
         
           
                 |
31 | 30 | ex 115 |
. . . . . . . 8
 
       
                             |
32 | 31 | exlimdvv 1897 |
. . . . . . 7
 
           
                             |
33 | 32 | adantr 276 |
. . . . . 6
                         
                             |
34 | 7, 33 | mpd 13 |
. . . . 5
                          
      |
35 | 1, 2 | genpprecll 7501 |
. . . . . . . . 9
 
      
    
               |
36 | 35 | imp 124 |
. . . . . . . 8
                             |
37 | | elprnql 7468 |
. . . . . . . . . . . . 13
                    |
38 | 8, 37 | sylan 283 |
. . . . . . . . . . . 12
 
       |
39 | | elprnql 7468 |
. . . . . . . . . . . . 13
                    |
40 | 11, 39 | sylan 283 |
. . . . . . . . . . . 12
 
       |
41 | 38, 40 | anim12i 338 |
. . . . . . . . . . 11
        
      
   |
42 | 41 | an4s 588 |
. . . . . . . . . 10
               
   |
43 | 2 | caovcl 6023 |
. . . . . . . . . 10
 
       |
44 | 42, 43 | syl 14 |
. . . . . . . . 9
                     |
45 | | breq2 4004 |
. . . . . . . . . . 11
     
       |
46 | | eleq1 2240 |
. . . . . . . . . . 11
             
               |
47 | 45, 46 | anbi12d 473 |
. . . . . . . . . 10
      
                              |
48 | 47 | adantl 277 |
. . . . . . . . 9
   

          
      
                              |
49 | 44, 48 | rspcedv 2845 |
. . . . . . . 8
                                 
 
            |
50 | 36, 49 | mpan2d 428 |
. . . . . . 7
                     
            |
51 | 50 | rexlimdvva 2602 |
. . . . . 6
 
                   
            |
52 | 51 | adantr 276 |
. . . . 5
                                 
            |
53 | 34, 52 | mpd 13 |
. . . 4
                
           |
54 | 53 | expr 375 |
. . 3
   
           
            |
55 | | genprndl.lower |
. . . . . . . . . . 11
   
           
                 |
56 | 1, 2, 55 | genpcdl 7506 |
. . . . . . . . . 10
 
                       |
57 | 56 | alrimdv 1876 |
. . . . . . . . 9
 
            
            |
58 | | breq1 4003 |
. . . . . . . . . . 11
 
   |
59 | | eleq1 2240 |
. . . . . . . . . . 11
         
           |
60 | 58, 59 | imbi12d 234 |
. . . . . . . . . 10
           

            |
61 | 60 | cbvalv 1917 |
. . . . . . . . 9
               
           |
62 | 57, 61 | syl6ib 161 |
. . . . . . . 8
 
            
            |
63 | | sp 1511 |
. . . . . . . 8
   
        

           |
64 | 62, 63 | syl6 33 |
. . . . . . 7
 
          
            |
65 | 64 | impd 254 |
. . . . . 6
 
           
           |
66 | 65 | ancomsd 269 |
. . . . 5
 
  
        
           |
67 | 66 | ad2antrr 488 |
. . . 4
   

   
                    |
68 | 67 | rexlimdva 2594 |
. . 3
   
   
        
           |
69 | 54, 68 | impbid 129 |
. 2
   
          

            |
70 | 69 | ralrimiva 2550 |
1
 
           

            |