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

  
                                      |
2 | 1 | relmptopab 6413 |
. . 3
cgrG   |
3 | 2 | a1i 11 |
. 2
 TarskiG
cgrG    |
4 | | ercgrg.p |
. . . . . . . . 9
     |
5 | | eqid 2452 |
. . . . . . . . 9
         |
6 | | eqid 2452 |
. . . . . . . . 9
cgrG  cgrG   |
7 | 4, 5, 6 | iscgrg 23096 |
. . . . . . . 8
 TarskiG   cgrG  
                                                 |
8 | 7 | biimpa 484 |
. . . . . . 7
  TarskiG
 cgrG      

    
 
                                     |
9 | 8 | simpld 459 |
. . . . . 6
  TarskiG
 cgrG            |
10 | 9 | simprd 463 |
. . . . 5
  TarskiG
 cgrG        |
11 | 9 | simpld 459 |
. . . . 5
  TarskiG
 cgrG        |
12 | 10, 11 | jca 532 |
. . . 4
  TarskiG
 cgrG            |
13 | 8 | simprd 463 |
. . . . . . 7
  TarskiG
 cgrG                                            |
14 | 13 | simpld 459 |
. . . . . 6
  TarskiG
 cgrG   
  |
15 | 14 | eqcomd 2460 |
. . . . 5
  TarskiG
 cgrG   
  |
16 | | simpl 457 |
. . . . . . . 8
   TarskiG  cgrG    
   TarskiG  cgrG      |
17 | | simprl 755 |
. . . . . . . . 9
   TarskiG  cgrG    
    |
18 | 16, 14 | syl 16 |
. . . . . . . . 9
   TarskiG  cgrG    
    |
19 | 17, 18 | eleqtrrd 2543 |
. . . . . . . 8
   TarskiG  cgrG    
    |
20 | | simprr 756 |
. . . . . . . . 9
   TarskiG  cgrG    
    |
21 | 20, 18 | eleqtrrd 2543 |
. . . . . . . 8
   TarskiG  cgrG    
    |
22 | 13 | simprd 463 |
. . . . . . . . . 10
  TarskiG
 cgrG                                          |
23 | 22 | r19.21bi 2914 |
. . . . . . . . 9
   TarskiG  cgrG     
                                   |
24 | 23 | r19.21bi 2914 |
. . . . . . . 8
    TarskiG  cgrG   
                                    |
25 | 16, 19, 21, 24 | syl21anc 1218 |
. . . . . . 7
   TarskiG  cgrG    
                                    |
26 | 25 | eqcomd 2460 |
. . . . . 6
   TarskiG  cgrG    
                                    |
27 | 26 | ralrimivva 2908 |
. . . . 5
  TarskiG
 cgrG                                          |
28 | 15, 27 | jca 532 |
. . . 4
  TarskiG
 cgrG    
                                       |
29 | 12, 28 | jca 532 |
. . 3
  TarskiG
 cgrG      

    
 
                                     |
30 | 4, 5, 6 | iscgrg 23096 |
. . . 4
 TarskiG   cgrG  
       
                                         |
31 | 30 | adantr 465 |
. . 3
  TarskiG
 cgrG      cgrG  
       
                                         |
32 | 29, 31 | mpbird 232 |
. 2
  TarskiG
 cgrG     cgrG     |
33 | 11 | adantrr 716 |
. . . . 5
  TarskiG
  cgrG    cgrG    
    |
34 | 4, 5, 6 | iscgrg 23096 |
. . . . . . . . 9
 TarskiG   cgrG  
       
                                         |
35 | 34 | biimpa 484 |
. . . . . . . 8
  TarskiG
 cgrG      

    
 
                                     |
36 | 35 | adantrl 715 |
. . . . . . 7
  TarskiG
  cgrG    cgrG         
 

  
                                     |
37 | 36 | simpld 459 |
. . . . . 6
  TarskiG
  cgrG    cgrG      

     |
38 | 37 | simprd 463 |
. . . . 5
  TarskiG
  cgrG    cgrG         |
39 | 33, 38 | jca 532 |
. . . 4
  TarskiG
  cgrG    cgrG      

     |
40 | 8 | adantrr 716 |
. . . . . . . 8
  TarskiG
  cgrG    cgrG         
 

  
                                     |
41 | 40 | simprd 463 |
. . . . . . 7
  TarskiG
  cgrG    cgrG     
                                       |
42 | 41 | simpld 459 |
. . . . . 6
  TarskiG
  cgrG    cgrG       |
43 | 36 | simprd 463 |
. . . . . . 7
  TarskiG
  cgrG    cgrG     
                                       |
44 | 43 | simpld 459 |
. . . . . 6
  TarskiG
  cgrG    cgrG    
  |
45 | 42, 44 | eqtrd 2493 |
. . . . 5
  TarskiG
  cgrG    cgrG       |
46 | 41 | simprd 463 |
. . . . . . . . . 10
  TarskiG
  cgrG    cgrG     
                                     |
47 | 46 | r19.21bi 2914 |
. . . . . . . . 9
   TarskiG   cgrG    cgrG    
                                     |
48 | 47 | r19.21bi 2914 |
. . . . . . . 8
    TarskiG   cgrG    cgrG    
                                    |
49 | 48 | anasss 647 |
. . . . . . 7
   TarskiG   cgrG    cgrG                                          |
50 | | simpl 457 |
. . . . . . . 8
   TarskiG   cgrG    cgrG         TarskiG   cgrG    cgrG       |
51 | | simprl 755 |
. . . . . . . . 9
   TarskiG   cgrG    cgrG          |
52 | 50, 42 | syl 16 |
. . . . . . . . 9
   TarskiG   cgrG    cgrG          |
53 | 51, 52 | eleqtrd 2542 |
. . . . . . . 8
   TarskiG   cgrG    cgrG          |
54 | | simprr 756 |
. . . . . . . . 9
   TarskiG   cgrG    cgrG          |
55 | 54, 52 | eleqtrd 2542 |
. . . . . . . 8
   TarskiG   cgrG    cgrG          |
56 | 43 | simprd 463 |
. . . . . . . . . 10
  TarskiG
  cgrG    cgrG     
                                     |
57 | 56 | r19.21bi 2914 |
. . . . . . . . 9
   TarskiG   cgrG    cgrG    
                                     |
58 | 57 | r19.21bi 2914 |
. . . . . . . 8
    TarskiG   cgrG    cgrG    
                                    |
59 | 50, 53, 55, 58 | syl21anc 1218 |
. . . . . . 7
   TarskiG   cgrG    cgrG                                          |
60 | 49, 59 | eqtrd 2493 |
. . . . . 6
   TarskiG   cgrG    cgrG                                          |
61 | 60 | ralrimivva 2908 |
. . . . 5
  TarskiG
  cgrG    cgrG     
                                     |
62 | 45, 61 | jca 532 |
. . . 4
  TarskiG
  cgrG    cgrG     
                                       |
63 | 39, 62 | jca 532 |
. . 3
  TarskiG
  cgrG    cgrG         
 

  
                                     |
64 | 4, 5, 6 | iscgrg 23096 |
. . . 4
 TarskiG   cgrG  
                                                 |
65 | 64 | adantr 465 |
. . 3
  TarskiG
  cgrG    cgrG       cgrG  
                                                 |
66 | 63, 65 | mpbird 232 |
. 2
  TarskiG
  cgrG    cgrG      cgrG     |
67 | 4, 5, 6 | iscgrg 23096 |
. . 3
 TarskiG   cgrG  
                                                 |
68 | | pm4.24 643 |
. . . 4
      
    |
69 | | eqid 2452 |
. . . . . 6
 |
70 | | eqidd 2453 |
. . . . . . 7
 
                                   |
71 | 70 | rgen2 2912 |
. . . . . 6
                                     |
72 | 69, 71 | pm3.2i 455 |
. . . . 5
                                       |
73 | 72 | biantru 505 |
. . . 4
      
                                                |
74 | 68, 73 | bitri 249 |
. . 3
                                                   |
75 | 67, 74 | syl6rbbr 264 |
. 2
 TarskiG     cgrG      |
76 | 3, 32, 66, 75 | iserd 7232 |
1
 TarskiG cgrG      |