Step | Hyp | Ref
| Expression |
1 | | eqid 2462 |
. . . . 5
         |
2 | | eqid 2462 |
. . . . 5
         |
3 | | eqid 2462 |
. . . . 5
         |
4 | | eqid 2462 |
. . . . 5
         |
5 | | eqid 2462 |
. . . . 5
.g  .g   |
6 | | simpll1 1053 |
. . . . 5
    oGrp oppg  oGrp
Archi
                                
        
oGrp |
7 | | simpll3 1055 |
. . . . 5
    oGrp oppg  oGrp
Archi
                                
        
Archi |
8 | | simplr 767 |
. . . . 5
    oGrp oppg  oGrp
Archi
                                
               |
9 | | simprl 769 |
. . . . 5
    oGrp oppg  oGrp
Archi
                                
                     |
10 | | simp2 1015 |
. . . . . 6
     oGrp
oppg  oGrp
Archi
                                
        
                     |
11 | | simp1rr 1080 |
. . . . . 6
     oGrp
oppg  oGrp
Archi
                                
        
                               
         |
12 | | simp3 1016 |
. . . . . 6
     oGrp
oppg  oGrp
Archi
                                
        
                           |
13 | | breq2 4420 |
. . . . . . . 8
           
             |
14 | | breq2 4420 |
. . . . . . . 8
       
         |
15 | 13, 14 | imbi12d 326 |
. . . . . . 7
                              
          |
16 | 15 | rspcv 3158 |
. . . . . 6
    
 
                                            |
17 | 10, 11, 12, 16 | syl3c 63 |
. . . . 5
     oGrp
oppg  oGrp
Archi
                                
        
                       |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 17 | archiabllem1 28559 |
. . . 4
    oGrp oppg  oGrp
Archi
                                
        
  |
19 | 18 | adantllr 730 |
. . 3
     oGrp
oppg  oGrp
Archi                  
                                                                  
  |
20 | | simpr 467 |
. . . 4
   oGrp oppg  oGrp
Archi 
                
                        
                                 
          |
21 | | breq2 4420 |
. . . . . 6
           
             |
22 | | breq1 4419 |
. . . . . . . 8
       
         |
23 | 22 | imbi2d 322 |
. . . . . . 7
                              
          |
24 | 23 | ralbidv 2839 |
. . . . . 6
  
                       
                          |
25 | 21, 24 | anbi12d 722 |
. . . . 5
                             
       
                           
           |
26 | 25 | cbvrexv 3032 |
. . . 4
                  
                        
                                           |
27 | 20, 26 | sylib 201 |
. . 3
   oGrp oppg  oGrp
Archi 
                
                        
                                 
          |
28 | 19, 27 | r19.29a 2944 |
. 2
   oGrp oppg  oGrp
Archi 
                
                        
  |
29 | | simpl1 1017 |
. . 3
   oGrp oppg  oGrp
Archi                  
                        
oGrp |
30 | | simpl3 1019 |
. . 3
   oGrp oppg  oGrp
Archi                  
                        
Archi |
31 | | eqid 2462 |
. . 3
       |
32 | | simpl2 1018 |
. . 3
   oGrp oppg  oGrp
Archi                  
                        
oppg  oGrp |
33 | | simpr 467 |
. . . . . . . . . 10
   oGrp oppg  oGrp
Archi                  
                        
                                 
          |
34 | | ralnex 2846 |
. . . . . . . . . 10
 
                                                                         
          |
35 | 33, 34 | sylibr 217 |
. . . . . . . . 9
   oGrp oppg  oGrp
Archi                  
                        
                
                          |
36 | | rexanali 2852 |
. . . . . . . . . . . 12
                                                   |
37 | 36 | imbi2i 318 |
. . . . . . . . . . 11
            
                                  
                
          |
38 | | imnan 428 |
. . . . . . . . . . 11
                                    
                                      |
39 | 37, 38 | bitri 257 |
. . . . . . . . . 10
            
                       
                           
          |
40 | 39 | ralbii 2831 |
. . . . . . . . 9
 
                                         
                               
          |
41 | 35, 40 | sylibr 217 |
. . . . . . . 8
   oGrp oppg  oGrp
Archi                  
                        
                
                           |
42 | 22 | notbid 300 |
. . . . . . . . . . . 12
       
         |
43 | 42 | anbi2d 715 |
. . . . . . . . . . 11
                   
                     |
44 | 43 | rexbidv 2913 |
. . . . . . . . . 10
  
                       
                          |
45 | 21, 44 | imbi12d 326 |
. . . . . . . . 9
                                     
          
                            |
46 | 45 | cbvralv 3031 |
. . . . . . . 8
 
                                         
                
                          |
47 | 41, 46 | sylib 201 |
. . . . . . 7
   oGrp oppg  oGrp
Archi                  
                        
                
                           |
48 | 47 | r19.21bi 2769 |
. . . . . 6
    oGrp oppg  oGrp
Archi                                  
        
                                           |
49 | 14 | notbid 300 |
. . . . . . . 8
       
         |
50 | 13, 49 | anbi12d 722 |
. . . . . . 7
                   
                     |
51 | 50 | cbvrexv 3032 |
. . . . . 6
                         
                         |
52 | 48, 51 | syl6ib 234 |
. . . . 5
    oGrp oppg  oGrp
Archi                                  
        
                                           |
53 | 52 | 3impia 1212 |
. . . 4
    oGrp oppg  oGrp
Archi                                  
        
                                         |
54 | | simp1l1 1107 |
. . . . . 6
    oGrp oppg  oGrp
Archi                                  
        
               oGrp |
55 | | isogrp 28514 |
. . . . . . 7
 oGrp  oMnd  |
56 | 55 | simprbi 470 |
. . . . . 6
 oGrp oMnd |
57 | | omndtos 28517 |
. . . . . 6
 oMnd Toset |
58 | 54, 56, 57 | 3syl 18 |
. . . . 5
    oGrp oppg  oGrp
Archi                                  
        
               Toset |
59 | | simp2 1015 |
. . . . 5
    oGrp oppg  oGrp
Archi                                  
        
                     |
60 | 1, 3, 4 | tltnle 28472 |
. . . . . . . . . 10
  Toset
   
    
      
         |
61 | 60 | bicomd 206 |
. . . . . . . . 9
  Toset
   
    
      
         |
62 | 61 | 3com23 1221 |
. . . . . . . 8
  Toset
   
    
      
         |
63 | 62 | 3expa 1215 |
. . . . . . 7
   Toset                 
         |
64 | 63 | anbi2d 715 |
. . . . . 6
   Toset                             
                     |
65 | 64 | rexbidva 2910 |
. . . . 5
  Toset
      
                       
                          |
66 | 58, 59, 65 | syl2anc 671 |
. . . 4
    oGrp oppg  oGrp
Archi                                  
        
                
                       
                          |
67 | 53, 66 | mpbid 215 |
. . 3
    oGrp oppg  oGrp
Archi                                  
        
                                         |
68 | 1, 2, 3, 4, 5, 29,
30, 31, 32, 67 | archiabllem2 28563 |
. 2
   oGrp oppg  oGrp
Archi                  
                        
  |
69 | 28, 68 | pm2.61dan 805 |
1
  oGrp oppg  oGrp
Archi
  |