Step | Hyp | Ref
| Expression |
1 | | prop 7184 |
. . . . . . . . 9
              |
2 | | elprnqu 7191 |
. . . . . . . . 9
                    |
3 | 1, 2 | sylan 279 |
. . . . . . . 8
 
       |
4 | | prop 7184 |
. . . . . . . . . . . . . . . 16
              |
5 | | elprnqu 7191 |
. . . . . . . . . . . . . . . 16
                    |
6 | 4, 5 | sylan 279 |
. . . . . . . . . . . . . . 15
 
       |
7 | | r19.41v 2545 |
. . . . . . . . . . . . . . . . 17
                
 
                |
8 | | prop 7184 |
. . . . . . . . . . . . . . . . . . . . 21
              |
9 | | elprnqu 7191 |
. . . . . . . . . . . . . . . . . . . . 21
                 
  |
10 | 8, 9 | sylan 279 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  |
11 | | oveq2 5714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
12 | 11 | adantr 272 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
 
              |
13 | | genpassg.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                   |
14 | 13 | adantl 273 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
 
                  |
15 | 12, 14 | eqtr4d 2135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
 
              |
16 | 15 | eqeq2d 2111 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
 
    
           |
17 | 16 | expcom 115 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                       |
18 | 17 | pm5.32d 441 |
. . . . . . . . . . . . . . . . . . . . 21
 
                             |
19 | 18 | 3expa 1149 |
. . . . . . . . . . . . . . . . . . . 20
   
           
                 |
20 | 10, 19 | sylan2 282 |
. . . . . . . . . . . . . . . . . . 19
                     
                 |
21 | 20 | anassrs 395 |
. . . . . . . . . . . . . . . . . 18
   

                                  |
22 | 21 | rexbidva 2393 |
. . . . . . . . . . . . . . . . 17
   
                 
                       |
23 | 7, 22 | syl5rbbr 194 |
. . . . . . . . . . . . . . . 16
   
                     
 
                 |
24 | 23 | an32s 538 |
. . . . . . . . . . . . . . 15
   
                     
 
                 |
25 | 6, 24 | sylan2 282 |
. . . . . . . . . . . . . 14
                               
 
                 |
26 | 25 | anassrs 395 |
. . . . . . . . . . . . 13
   

       
         
                            |
27 | 26 | rexbidva 2393 |
. . . . . . . . . . . 12
   
                           
                         |
28 | | r19.41v 2545 |
. . . . . . . . . . . 12
                      
 
                      |
29 | 27, 28 | syl6bb 195 |
. . . . . . . . . . 11
   
                           
 
                       |
30 | 29 | an31s 540 |
. . . . . . . . . 10
   
                           
 
                       |
31 | 30 | exbidv 1764 |
. . . . . . . . 9
   
    
                        
                           |
32 | | genpelvl.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
33 | 32 | caovcl 5857 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
34 | | elisset 2655 |
. . . . . . . . . . . . . . . . . . . . . . 23
            |
35 | 33, 34 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
 
        |
36 | 35 | biantrurd 301 |
. . . . . . . . . . . . . . . . . . . . 21
 
                            |
37 | | 19.41v 1841 |
. . . . . . . . . . . . . . . . . . . . 21
                
 
               |
38 | 36, 37 | syl6bbr 197 |
. . . . . . . . . . . . . . . . . . . 20
 
                             |
39 | 10, 38 | sylan2 282 |
. . . . . . . . . . . . . . . . . . 19
  
                                  |
40 | 39 | anassrs 395 |
. . . . . . . . . . . . . . . . . 18
   
                                 |
41 | 40 | rexbidva 2393 |
. . . . . . . . . . . . . . . . 17
 
                
                        |
42 | | rexcom4 2664 |
. . . . . . . . . . . . . . . . 17
                                               |
43 | 41, 42 | syl6bb 195 |
. . . . . . . . . . . . . . . 16
 
                                         |
44 | 43 | ancoms 266 |
. . . . . . . . . . . . . . 15
 
                                         |
45 | 6, 44 | sylan2 282 |
. . . . . . . . . . . . . 14
  
                                              |
46 | 45 | anassrs 395 |
. . . . . . . . . . . . 13
   
                                             |
47 | 46 | rexbidva 2393 |
. . . . . . . . . . . 12
 
                      
                              |
48 | 47 | ancoms 266 |
. . . . . . . . . . 11
 
                      
                              |
49 | | rexcom4 2664 |
. . . . . . . . . . 11
         
         
                                       |
50 | 48, 49 | syl6bb 195 |
. . . . . . . . . 10
 
                                                     |
51 | 50 | adantr 272 |
. . . . . . . . 9
   
                                                     |
52 | | df-rex 2381 |
. . . . . . . . . . 11
                                 |
53 | | genpelvl.1 |
. . . . . . . . . . . . . 14
 
            
       
          
         |
54 | 53, 32 | genpelvu 7222 |
. . . . . . . . . . . . 13
 
          
                  |
55 | 54 | anbi1d 456 |
. . . . . . . . . . . 12
 
                                         |
56 | 55 | exbidv 1764 |
. . . . . . . . . . 11
 
                 
                           |
57 | 52, 56 | syl5bb 191 |
. . . . . . . . . 10
 
               
                           |
58 | 57 | adantr 272 |
. . . . . . . . 9
   
               
                           |
59 | 31, 51, 58 | 3bitr4rd 220 |
. . . . . . . 8
   
               
                       |
60 | 3, 59 | sylan2 282 |
. . . . . . 7
                         
                       |
61 | 60 | anassrs 395 |
. . . . . 6
   

       
            
                       |
62 | 61 | rexbidva 2393 |
. . . . 5
   
                     
                             |
63 | 62 | ancoms 266 |
. . . 4
  
 
 
                  
                             |
64 | 63 | 3impb 1145 |
. . 3
 
  
                                                |
65 | | genpassg.5 |
. . . . . 6
 
       |
66 | 65 | caovcl 5857 |
. . . . 5
 
       |
67 | 53, 32 | genpelvu 7222 |
. . . . 5
                    
                      |
68 | 66, 67 | sylan2 282 |
. . . 4
  
 
             
                      |
69 | 68 | 3impb 1145 |
. . 3
 
             
                       |
70 | | df-rex 2381 |
. . . . 5
                                             |
71 | 53, 32 | genpelvu 7222 |
. . . . . . . 8
 
          
                  |
72 | 71 | 3adant3 969 |
. . . . . . 7
 
         
                   |
73 | 72 | anbi1d 456 |
. . . . . 6
 
                                                     |
74 | 73 | exbidv 1764 |
. . . . 5
 
                                                         |
75 | 70, 74 | syl5bb 191 |
. . . 4
 
  
                                                    |
76 | 65 | caovcl 5857 |
. . . . . 6
 
       |
77 | 53, 32 | genpelvu 7222 |
. . . . . 6
     
              
                      |
78 | 76, 77 | sylan 279 |
. . . . 5
   
                                     |
79 | 78 | 3impa 1144 |
. . . 4
 
             
                       |
80 | 32 | caovcl 5857 |
. . . . . . . . . . . . . . . . . . 19
 
       |
81 | | elisset 2655 |
. . . . . . . . . . . . . . . . . . 19
            |
82 | 80, 81 | syl 14 |
. . . . . . . . . . . . . . . . . 18
 
        |
83 | 82 | biantrurd 301 |
. . . . . . . . . . . . . . . . 17
 
                      
                 |
84 | | oveq1 5713 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
85 | 84 | eqeq2d 2111 |
. . . . . . . . . . . . . . . . . . . . 21
         
           |
86 | 85 | rexbidv 2397 |
. . . . . . . . . . . . . . . . . . . 20
      
        
                 |
87 | 86 | pm5.32i 445 |
. . . . . . . . . . . . . . . . . . 19
                
     
                |
88 | 87 | exbii 1552 |
. . . . . . . . . . . . . . . . . 18
                          
                |
89 | | 19.41v 1841 |
. . . . . . . . . . . . . . . . . 18
                                              |
90 | 88, 89 | bitri 183 |
. . . . . . . . . . . . . . . . 17
                                          |
91 | 83, 90 | syl6bbr 197 |
. . . . . . . . . . . . . . . 16
 
                                     |
92 | 6, 91 | sylan2 282 |
. . . . . . . . . . . . . . 15
  
                                          |
93 | 92 | anassrs 395 |
. . . . . . . . . . . . . 14
   
                                         |
94 | 93 | rexbidva 2393 |
. . . . . . . . . . . . 13
 
                      
                          |
95 | | rexcom4 2664 |
. . . . . . . . . . . . 13
                                                   |
96 | 94, 95 | syl6bb 195 |
. . . . . . . . . . . 12
 
                                                 |
97 | 96 | ancoms 266 |
. . . . . . . . . . 11
 
                                                 |
98 | 3, 97 | sylan2 282 |
. . . . . . . . . 10
  
                                                      |
99 | 98 | anassrs 395 |
. . . . . . . . 9
   
                                                     |
100 | 99 | rexbidva 2393 |
. . . . . . . 8
 
                            
                                |
101 | | rexcom4 2664 |
. . . . . . . 8
         
                    
  
                
            |
102 | 100, 101 | syl6bb 195 |
. . . . . . 7
 
                                                             |
103 | | r19.41v 2545 |
. . . . . . . . . 10
            
         
 
                      |
104 | 103 | rexbii 2401 |
. . . . . . . . 9
                                                           |
105 | | r19.41v 2545 |
. . . . . . . . 9
                                                           |
106 | 104, 105 | bitri 183 |
. . . . . . . 8
                                                           |
107 | 106 | exbii 1552 |
. . . . . . 7
                                                               |
108 | 102, 107 | syl6bb 195 |
. . . . . 6
 
                                                             |
109 | 108 | ancoms 266 |
. . . . 5
 
                                                             |
110 | 109 | 3adant3 969 |
. . . 4
 
  
                                                          |
111 | 75, 79, 110 | 3bitr4d 219 |
. . 3
 
             
                             |
112 | 64, 69, 111 | 3bitr4rd 220 |
. 2
 
             
               |
113 | 112 | eqrdv 2098 |
1
 
                           |