Step | Hyp | Ref
| Expression |
1 | | df-cgrg 27762 |
. . . 4
β’ cgrG =
(π β V β¦
{β¨π, πβ© β£ ((π β ((Baseβπ) βpm β)
β§ π β
((Baseβπ)
βpm β)) β§ (dom π = dom π β§ βπ β dom πβπ β dom π((πβπ)(distβπ)(πβπ)) = ((πβπ)(distβπ)(πβπ))))}) |
2 | 1 | relmptopab 7656 |
. . 3
β’ Rel
(cgrGβπΊ) |
3 | 2 | a1i 11 |
. 2
β’ (πΊ β TarskiG β Rel
(cgrGβπΊ)) |
4 | | ercgrg.p |
. . . . . . 7
β’ π = (BaseβπΊ) |
5 | | eqid 2733 |
. . . . . . 7
β’
(distβπΊ) =
(distβπΊ) |
6 | | eqid 2733 |
. . . . . . 7
β’
(cgrGβπΊ) =
(cgrGβπΊ) |
7 | 4, 5, 6 | iscgrg 27763 |
. . . . . 6
β’ (πΊ β TarskiG β (π₯(cgrGβπΊ)π¦ β ((π₯ β (π βpm β) β§ π¦ β (π βpm β)) β§ (dom
π₯ = dom π¦ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ)))))) |
8 | 7 | biimpa 478 |
. . . . 5
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β ((π₯ β (π βpm β) β§ π¦ β (π βpm β)) β§ (dom
π₯ = dom π¦ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))))) |
9 | 8 | simpld 496 |
. . . 4
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β (π₯ β (π βpm β) β§ π¦ β (π βpm
β))) |
10 | 9 | ancomd 463 |
. . 3
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β (π¦ β (π βpm β) β§ π₯ β (π βpm
β))) |
11 | 8 | simprd 497 |
. . . . . 6
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β (dom π₯ = dom π¦ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ)))) |
12 | 11 | simpld 496 |
. . . . 5
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β dom π₯ = dom π¦) |
13 | 12 | eqcomd 2739 |
. . . 4
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β dom π¦ = dom π₯) |
14 | | simpl 484 |
. . . . . . 7
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ (π β dom π¦ β§ π β dom π¦)) β (πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦)) |
15 | | simprl 770 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ (π β dom π¦ β§ π β dom π¦)) β π β dom π¦) |
16 | 12 | adantr 482 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ (π β dom π¦ β§ π β dom π¦)) β dom π₯ = dom π¦) |
17 | 15, 16 | eleqtrrd 2837 |
. . . . . . 7
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ (π β dom π¦ β§ π β dom π¦)) β π β dom π₯) |
18 | | simprr 772 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ (π β dom π¦ β§ π β dom π¦)) β π β dom π¦) |
19 | 18, 16 | eleqtrrd 2837 |
. . . . . . 7
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ (π β dom π¦ β§ π β dom π¦)) β π β dom π₯) |
20 | 11 | simprd 497 |
. . . . . . . . 9
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))) |
21 | 20 | r19.21bi 3249 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ π β dom π₯) β βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))) |
22 | 21 | r19.21bi 3249 |
. . . . . . 7
β’ ((((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ π β dom π₯) β§ π β dom π₯) β ((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))) |
23 | 14, 17, 19, 22 | syl21anc 837 |
. . . . . 6
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ (π β dom π¦ β§ π β dom π¦)) β ((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))) |
24 | 23 | eqcomd 2739 |
. . . . 5
β’ (((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β§ (π β dom π¦ β§ π β dom π¦)) β ((π¦βπ)(distβπΊ)(π¦βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ))) |
25 | 24 | ralrimivva 3201 |
. . . 4
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ))) |
26 | 13, 25 | jca 513 |
. . 3
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β (dom π¦ = dom π₯ β§ βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ)))) |
27 | 4, 5, 6 | iscgrg 27763 |
. . . 4
β’ (πΊ β TarskiG β (π¦(cgrGβπΊ)π₯ β ((π¦ β (π βpm β) β§ π₯ β (π βpm β)) β§ (dom
π¦ = dom π₯ β§ βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ)))))) |
28 | 27 | adantr 482 |
. . 3
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β (π¦(cgrGβπΊ)π₯ β ((π¦ β (π βpm β) β§ π₯ β (π βpm β)) β§ (dom
π¦ = dom π₯ β§ βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ)))))) |
29 | 10, 26, 28 | mpbir2and 712 |
. 2
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β π¦(cgrGβπΊ)π₯) |
30 | 9 | simpld 496 |
. . . . 5
β’ ((πΊ β TarskiG β§ π₯(cgrGβπΊ)π¦) β π₯ β (π βpm
β)) |
31 | 30 | adantrr 716 |
. . . 4
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β π₯ β (π βpm
β)) |
32 | 4, 5, 6 | iscgrg 27763 |
. . . . . . . 8
β’ (πΊ β TarskiG β (π¦(cgrGβπΊ)π§ β ((π¦ β (π βpm β) β§ π§ β (π βpm β)) β§ (dom
π¦ = dom π§ β§ βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π§βπ)(distβπΊ)(π§βπ)))))) |
33 | 32 | biimpa 478 |
. . . . . . 7
β’ ((πΊ β TarskiG β§ π¦(cgrGβπΊ)π§) β ((π¦ β (π βpm β) β§ π§ β (π βpm β)) β§ (dom
π¦ = dom π§ β§ βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π§βπ)(distβπΊ)(π§βπ))))) |
34 | 33 | adantrl 715 |
. . . . . 6
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β ((π¦ β (π βpm β) β§ π§ β (π βpm β)) β§ (dom
π¦ = dom π§ β§ βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π§βπ)(distβπΊ)(π§βπ))))) |
35 | 34 | simpld 496 |
. . . . 5
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β (π¦ β (π βpm β) β§ π§ β (π βpm
β))) |
36 | 35 | simprd 497 |
. . . 4
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β π§ β (π βpm
β)) |
37 | 31, 36 | jca 513 |
. . 3
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β (π₯ β (π βpm β) β§ π§ β (π βpm
β))) |
38 | 8 | adantrr 716 |
. . . . . . 7
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β ((π₯ β (π βpm β) β§ π¦ β (π βpm β)) β§ (dom
π₯ = dom π¦ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))))) |
39 | 38 | simprd 497 |
. . . . . 6
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β (dom π₯ = dom π¦ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ)))) |
40 | 39 | simpld 496 |
. . . . 5
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β dom π₯ = dom π¦) |
41 | 34 | simprd 497 |
. . . . . 6
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β (dom π¦ = dom π§ β§ βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π§βπ)(distβπΊ)(π§βπ)))) |
42 | 41 | simpld 496 |
. . . . 5
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β dom π¦ = dom π§) |
43 | 40, 42 | eqtrd 2773 |
. . . 4
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β dom π₯ = dom π§) |
44 | 39 | simprd 497 |
. . . . . . . . 9
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))) |
45 | 44 | r19.21bi 3249 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ π β dom π₯) β βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))) |
46 | 45 | r19.21bi 3249 |
. . . . . . 7
β’ ((((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ π β dom π₯) β§ π β dom π₯) β ((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))) |
47 | 46 | anasss 468 |
. . . . . 6
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β ((π₯βπ)(distβπΊ)(π₯βπ)) = ((π¦βπ)(distβπΊ)(π¦βπ))) |
48 | | simpl 484 |
. . . . . . 7
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β (πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§))) |
49 | | simprl 770 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β π β dom π₯) |
50 | 40 | adantr 482 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β dom π₯ = dom π¦) |
51 | 49, 50 | eleqtrd 2836 |
. . . . . . 7
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β π β dom π¦) |
52 | | simprr 772 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β π β dom π₯) |
53 | 52, 50 | eleqtrd 2836 |
. . . . . . 7
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β π β dom π¦) |
54 | 41 | simprd 497 |
. . . . . . . . 9
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β βπ β dom π¦βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π§βπ)(distβπΊ)(π§βπ))) |
55 | 54 | r19.21bi 3249 |
. . . . . . . 8
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ π β dom π¦) β βπ β dom π¦((π¦βπ)(distβπΊ)(π¦βπ)) = ((π§βπ)(distβπΊ)(π§βπ))) |
56 | 55 | r19.21bi 3249 |
. . . . . . 7
β’ ((((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ π β dom π¦) β§ π β dom π¦) β ((π¦βπ)(distβπΊ)(π¦βπ)) = ((π§βπ)(distβπΊ)(π§βπ))) |
57 | 48, 51, 53, 56 | syl21anc 837 |
. . . . . 6
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β ((π¦βπ)(distβπΊ)(π¦βπ)) = ((π§βπ)(distβπΊ)(π§βπ))) |
58 | 47, 57 | eqtrd 2773 |
. . . . 5
β’ (((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β§ (π β dom π₯ β§ π β dom π₯)) β ((π₯βπ)(distβπΊ)(π₯βπ)) = ((π§βπ)(distβπΊ)(π§βπ))) |
59 | 58 | ralrimivva 3201 |
. . . 4
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π§βπ)(distβπΊ)(π§βπ))) |
60 | 43, 59 | jca 513 |
. . 3
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β (dom π₯ = dom π§ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π§βπ)(distβπΊ)(π§βπ)))) |
61 | 4, 5, 6 | iscgrg 27763 |
. . . 4
β’ (πΊ β TarskiG β (π₯(cgrGβπΊ)π§ β ((π₯ β (π βpm β) β§ π§ β (π βpm β)) β§ (dom
π₯ = dom π§ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π§βπ)(distβπΊ)(π§βπ)))))) |
62 | 61 | adantr 482 |
. . 3
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β (π₯(cgrGβπΊ)π§ β ((π₯ β (π βpm β) β§ π§ β (π βpm β)) β§ (dom
π₯ = dom π§ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π§βπ)(distβπΊ)(π§βπ)))))) |
63 | 37, 60, 62 | mpbir2and 712 |
. 2
β’ ((πΊ β TarskiG β§ (π₯(cgrGβπΊ)π¦ β§ π¦(cgrGβπΊ)π§)) β π₯(cgrGβπΊ)π§) |
64 | | pm4.24 565 |
. . . 4
β’ (π₯ β (π βpm β) β (π₯ β (π βpm β) β§ π₯ β (π βpm
β))) |
65 | | eqid 2733 |
. . . . . 6
β’ dom π₯ = dom π₯ |
66 | | eqidd 2734 |
. . . . . . 7
β’ ((π β dom π₯ β§ π β dom π₯) β ((π₯βπ)(distβπΊ)(π₯βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ))) |
67 | 66 | rgen2 3198 |
. . . . . 6
β’
βπ β dom
π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ)) |
68 | 65, 67 | pm3.2i 472 |
. . . . 5
β’ (dom
π₯ = dom π₯ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ))) |
69 | 68 | biantru 531 |
. . . 4
β’ ((π₯ β (π βpm β) β§ π₯ β (π βpm β)) β
((π₯ β (π βpm β)
β§ π₯ β (π βpm β))
β§ (dom π₯ = dom π₯ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ))))) |
70 | 64, 69 | bitri 275 |
. . 3
β’ (π₯ β (π βpm β) β ((π₯ β (π βpm β) β§ π₯ β (π βpm β)) β§ (dom
π₯ = dom π₯ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ))))) |
71 | 4, 5, 6 | iscgrg 27763 |
. . 3
β’ (πΊ β TarskiG β (π₯(cgrGβπΊ)π₯ β ((π₯ β (π βpm β) β§ π₯ β (π βpm β)) β§ (dom
π₯ = dom π₯ β§ βπ β dom π₯βπ β dom π₯((π₯βπ)(distβπΊ)(π₯βπ)) = ((π₯βπ)(distβπΊ)(π₯βπ)))))) |
72 | 70, 71 | bitr4id 290 |
. 2
β’ (πΊ β TarskiG β (π₯ β (π βpm β) β π₯(cgrGβπΊ)π₯)) |
73 | 3, 29, 63, 72 | iserd 8729 |
1
β’ (πΊ β TarskiG β
(cgrGβπΊ) Er (π βpm
β)) |