Step | Hyp | Ref
| Expression |
1 | | df-cgrg 25406 |
. . . 4
cgrG
|
2 | 1 | relmptopab 6883 |
. . 3
cgrG |
3 | 2 | a1i 11 |
. 2
TarskiG
cgrG |
4 | | ercgrg.p |
. . . . . . 7
|
5 | | eqid 2622 |
. . . . . . 7
|
6 | | eqid 2622 |
. . . . . . 7
cgrG cgrG |
7 | 4, 5, 6 | iscgrg 25407 |
. . . . . 6
TarskiG cgrG
|
8 | 7 | biimpa 501 |
. . . . 5
TarskiG
cgrG
|
9 | 8 | simpld 475 |
. . . 4
TarskiG
cgrG |
10 | 9 | ancomd 467 |
. . 3
TarskiG
cgrG |
11 | 8 | simprd 479 |
. . . . . 6
TarskiG
cgrG |
12 | 11 | simpld 475 |
. . . . 5
TarskiG
cgrG
|
13 | 12 | eqcomd 2628 |
. . . 4
TarskiG
cgrG
|
14 | | simpl 473 |
. . . . . . 7
TarskiG cgrG
TarskiG cgrG |
15 | | simprl 794 |
. . . . . . . 8
TarskiG cgrG
|
16 | 12 | adantr 481 |
. . . . . . . 8
TarskiG cgrG
|
17 | 15, 16 | eleqtrrd 2704 |
. . . . . . 7
TarskiG cgrG
|
18 | | simprr 796 |
. . . . . . . 8
TarskiG cgrG
|
19 | 18, 16 | eleqtrrd 2704 |
. . . . . . 7
TarskiG cgrG
|
20 | 11 | simprd 479 |
. . . . . . . . 9
TarskiG
cgrG |
21 | 20 | r19.21bi 2932 |
. . . . . . . 8
TarskiG cgrG
|
22 | 21 | r19.21bi 2932 |
. . . . . . 7
TarskiG cgrG
|
23 | 14, 17, 19, 22 | syl21anc 1325 |
. . . . . 6
TarskiG cgrG
|
24 | 23 | eqcomd 2628 |
. . . . 5
TarskiG cgrG
|
25 | 24 | ralrimivva 2971 |
. . . 4
TarskiG
cgrG |
26 | 13, 25 | jca 554 |
. . 3
TarskiG
cgrG
|
27 | 4, 5, 6 | iscgrg 25407 |
. . . 4
TarskiG cgrG
|
28 | 27 | adantr 481 |
. . 3
TarskiG
cgrG cgrG
|
29 | 10, 26, 28 | mpbir2and 957 |
. 2
TarskiG
cgrG cgrG |
30 | 9 | simpld 475 |
. . . . 5
TarskiG
cgrG |
31 | 30 | adantrr 753 |
. . . 4
TarskiG
cgrG cgrG
|
32 | 4, 5, 6 | iscgrg 25407 |
. . . . . . . 8
TarskiG cgrG
|
33 | 32 | biimpa 501 |
. . . . . . 7
TarskiG
cgrG
|
34 | 33 | adantrl 752 |
. . . . . 6
TarskiG
cgrG cgrG
|
35 | 34 | simpld 475 |
. . . . 5
TarskiG
cgrG cgrG
|
36 | 35 | simprd 479 |
. . . 4
TarskiG
cgrG cgrG |
37 | 31, 36 | jca 554 |
. . 3
TarskiG
cgrG cgrG
|
38 | 8 | adantrr 753 |
. . . . . . 7
TarskiG
cgrG cgrG
|
39 | 38 | simprd 479 |
. . . . . 6
TarskiG
cgrG cgrG
|
40 | 39 | simpld 475 |
. . . . 5
TarskiG
cgrG cgrG |
41 | 34 | simprd 479 |
. . . . . 6
TarskiG
cgrG cgrG
|
42 | 41 | simpld 475 |
. . . . 5
TarskiG
cgrG cgrG
|
43 | 40, 42 | eqtrd 2656 |
. . . 4
TarskiG
cgrG cgrG |
44 | 39 | simprd 479 |
. . . . . . . . 9
TarskiG
cgrG cgrG
|
45 | 44 | r19.21bi 2932 |
. . . . . . . 8
TarskiG cgrG cgrG
|
46 | 45 | r19.21bi 2932 |
. . . . . . 7
TarskiG cgrG cgrG
|
47 | 46 | anasss 679 |
. . . . . 6
TarskiG cgrG cgrG |
48 | | simpl 473 |
. . . . . . 7
TarskiG cgrG cgrG TarskiG cgrG cgrG |
49 | | simprl 794 |
. . . . . . . 8
TarskiG cgrG cgrG |
50 | 40 | adantr 481 |
. . . . . . . 8
TarskiG cgrG cgrG |
51 | 49, 50 | eleqtrd 2703 |
. . . . . . 7
TarskiG cgrG cgrG |
52 | | simprr 796 |
. . . . . . . 8
TarskiG cgrG cgrG |
53 | 52, 50 | eleqtrd 2703 |
. . . . . . 7
TarskiG cgrG cgrG |
54 | 41 | simprd 479 |
. . . . . . . . 9
TarskiG
cgrG cgrG
|
55 | 54 | r19.21bi 2932 |
. . . . . . . 8
TarskiG cgrG cgrG
|
56 | 55 | r19.21bi 2932 |
. . . . . . 7
TarskiG cgrG cgrG
|
57 | 48, 51, 53, 56 | syl21anc 1325 |
. . . . . 6
TarskiG cgrG cgrG |
58 | 47, 57 | eqtrd 2656 |
. . . . 5
TarskiG cgrG cgrG |
59 | 58 | ralrimivva 2971 |
. . . 4
TarskiG
cgrG cgrG
|
60 | 43, 59 | jca 554 |
. . 3
TarskiG
cgrG cgrG
|
61 | 4, 5, 6 | iscgrg 25407 |
. . . 4
TarskiG cgrG
|
62 | 61 | adantr 481 |
. . 3
TarskiG
cgrG cgrG cgrG
|
63 | 37, 60, 62 | mpbir2and 957 |
. 2
TarskiG
cgrG cgrG cgrG |
64 | 4, 5, 6 | iscgrg 25407 |
. . 3
TarskiG cgrG
|
65 | | pm4.24 675 |
. . . 4
|
66 | | eqid 2622 |
. . . . . 6
|
67 | | eqidd 2623 |
. . . . . . 7
|
68 | 67 | rgen2a 2977 |
. . . . . 6
|
69 | 66, 68 | pm3.2i 471 |
. . . . 5
|
70 | 69 | biantru 526 |
. . . 4
|
71 | 65, 70 | bitri 264 |
. . 3
|
72 | 64, 71 | syl6rbbr 279 |
. 2
TarskiG cgrG |
73 | 3, 29, 63, 72 | iserd 7768 |
1
TarskiG cgrG |