Step | Hyp | Ref
| Expression |
1 | | df-cgrg 24635 |
. . . 4
cgrG                  
 

  
                                      |
2 | 1 | relmptopab 6536 |
. . 3
cgrG   |
3 | 2 | a1i 11 |
. 2
 TarskiG
cgrG    |
4 | | ercgrg.p |
. . . . . . 7
     |
5 | | eqid 2471 |
. . . . . . 7
         |
6 | | eqid 2471 |
. . . . . . 7
cgrG  cgrG   |
7 | 4, 5, 6 | iscgrg 24636 |
. . . . . 6
 TarskiG   cgrG  
                                                 |
8 | 7 | biimpa 492 |
. . . . 5
  TarskiG
 cgrG      

    
 
                                     |
9 | 8 | simpld 466 |
. . . 4
  TarskiG
 cgrG            |
10 | 9 | ancomd 458 |
. . 3
  TarskiG
 cgrG            |
11 | 8 | simprd 470 |
. . . . . 6
  TarskiG
 cgrG                                            |
12 | 11 | simpld 466 |
. . . . 5
  TarskiG
 cgrG   
  |
13 | 12 | eqcomd 2477 |
. . . 4
  TarskiG
 cgrG   
  |
14 | | simpl 464 |
. . . . . . 7
   TarskiG  cgrG    
   TarskiG  cgrG      |
15 | | simprl 772 |
. . . . . . . 8
   TarskiG  cgrG    
    |
16 | 12 | adantr 472 |
. . . . . . . 8
   TarskiG  cgrG    
    |
17 | 15, 16 | eleqtrrd 2552 |
. . . . . . 7
   TarskiG  cgrG    
    |
18 | | simprr 774 |
. . . . . . . 8
   TarskiG  cgrG    
    |
19 | 18, 16 | eleqtrrd 2552 |
. . . . . . 7
   TarskiG  cgrG    
    |
20 | 11 | simprd 470 |
. . . . . . . . 9
  TarskiG
 cgrG                                          |
21 | 20 | r19.21bi 2776 |
. . . . . . . 8
   TarskiG  cgrG     
                                   |
22 | 21 | r19.21bi 2776 |
. . . . . . 7
    TarskiG  cgrG   
                                    |
23 | 14, 17, 19, 22 | syl21anc 1291 |
. . . . . 6
   TarskiG  cgrG    
                                    |
24 | 23 | eqcomd 2477 |
. . . . 5
   TarskiG  cgrG    
                                    |
25 | 24 | ralrimivva 2814 |
. . . 4
  TarskiG
 cgrG                                          |
26 | 13, 25 | jca 541 |
. . 3
  TarskiG
 cgrG    
                                       |
27 | 4, 5, 6 | iscgrg 24636 |
. . . 4
 TarskiG   cgrG  
       
                                         |
28 | 27 | adantr 472 |
. . 3
  TarskiG
 cgrG      cgrG  
       
                                         |
29 | 10, 26, 28 | mpbir2and 936 |
. 2
  TarskiG
 cgrG     cgrG     |
30 | 9 | simpld 466 |
. . . . 5
  TarskiG
 cgrG        |
31 | 30 | adantrr 731 |
. . . 4
  TarskiG
  cgrG    cgrG    
    |
32 | 4, 5, 6 | iscgrg 24636 |
. . . . . . . 8
 TarskiG   cgrG  
       
                                         |
33 | 32 | biimpa 492 |
. . . . . . 7
  TarskiG
 cgrG      

    
 
                                     |
34 | 33 | adantrl 730 |
. . . . . 6
  TarskiG
  cgrG    cgrG         
 

  
                                     |
35 | 34 | simpld 466 |
. . . . 5
  TarskiG
  cgrG    cgrG      

     |
36 | 35 | simprd 470 |
. . . 4
  TarskiG
  cgrG    cgrG         |
37 | 31, 36 | jca 541 |
. . 3
  TarskiG
  cgrG    cgrG      

     |
38 | 8 | adantrr 731 |
. . . . . . 7
  TarskiG
  cgrG    cgrG         
 

  
                                     |
39 | 38 | simprd 470 |
. . . . . 6
  TarskiG
  cgrG    cgrG     
                                       |
40 | 39 | simpld 466 |
. . . . 5
  TarskiG
  cgrG    cgrG       |
41 | 34 | simprd 470 |
. . . . . 6
  TarskiG
  cgrG    cgrG     
                                       |
42 | 41 | simpld 466 |
. . . . 5
  TarskiG
  cgrG    cgrG    
  |
43 | 40, 42 | eqtrd 2505 |
. . . 4
  TarskiG
  cgrG    cgrG       |
44 | 39 | simprd 470 |
. . . . . . . . 9
  TarskiG
  cgrG    cgrG     
                                     |
45 | 44 | r19.21bi 2776 |
. . . . . . . 8
   TarskiG   cgrG    cgrG    
                                     |
46 | 45 | r19.21bi 2776 |
. . . . . . 7
    TarskiG   cgrG    cgrG    
                                    |
47 | 46 | anasss 659 |
. . . . . 6
   TarskiG   cgrG    cgrG                                          |
48 | | simpl 464 |
. . . . . . 7
   TarskiG   cgrG    cgrG         TarskiG   cgrG    cgrG       |
49 | | simprl 772 |
. . . . . . . 8
   TarskiG   cgrG    cgrG          |
50 | 40 | adantr 472 |
. . . . . . . 8
   TarskiG   cgrG    cgrG          |
51 | 49, 50 | eleqtrd 2551 |
. . . . . . 7
   TarskiG   cgrG    cgrG          |
52 | | simprr 774 |
. . . . . . . 8
   TarskiG   cgrG    cgrG          |
53 | 52, 50 | eleqtrd 2551 |
. . . . . . 7
   TarskiG   cgrG    cgrG          |
54 | 41 | simprd 470 |
. . . . . . . . 9
  TarskiG
  cgrG    cgrG     
                                     |
55 | 54 | r19.21bi 2776 |
. . . . . . . 8
   TarskiG   cgrG    cgrG    
                                     |
56 | 55 | r19.21bi 2776 |
. . . . . . 7
    TarskiG   cgrG    cgrG    
                                    |
57 | 48, 51, 53, 56 | syl21anc 1291 |
. . . . . 6
   TarskiG   cgrG    cgrG                                          |
58 | 47, 57 | eqtrd 2505 |
. . . . 5
   TarskiG   cgrG    cgrG                                          |
59 | 58 | ralrimivva 2814 |
. . . 4
  TarskiG
  cgrG    cgrG     
                                     |
60 | 43, 59 | jca 541 |
. . 3
  TarskiG
  cgrG    cgrG     
                                       |
61 | 4, 5, 6 | iscgrg 24636 |
. . . 4
 TarskiG   cgrG  
                                                 |
62 | 61 | adantr 472 |
. . 3
  TarskiG
  cgrG    cgrG       cgrG  
                                                 |
63 | 37, 60, 62 | mpbir2and 936 |
. 2
  TarskiG
  cgrG    cgrG      cgrG     |
64 | 4, 5, 6 | iscgrg 24636 |
. . 3
 TarskiG   cgrG  
                                                 |
65 | | pm4.24 655 |
. . . 4
      
    |
66 | | eqid 2471 |
. . . . . 6
 |
67 | | eqidd 2472 |
. . . . . . 7
 
                                   |
68 | 67 | rgen2a 2820 |
. . . . . 6
                                     |
69 | 66, 68 | pm3.2i 462 |
. . . . 5
                                       |
70 | 69 | biantru 513 |
. . . 4
      
                                                |
71 | 65, 70 | bitri 257 |
. . 3
                                                   |
72 | 64, 71 | syl6rbbr 272 |
. 2
 TarskiG     cgrG      |
73 | 3, 29, 63, 72 | iserd 7407 |
1
 TarskiG cgrG      |