Step | Hyp | Ref
| Expression |
1 | | df-trkg 27395 |
. . . . 5
β’ TarskiG =
((TarskiGC β© TarskiGB) β© (TarskiGCB
β© {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) |
2 | | inss1 4188 |
. . . . . 6
β’
((TarskiGC β© TarskiGB) β©
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) β (TarskiGC β©
TarskiGB) |
3 | | inss1 4188 |
. . . . . 6
β’
(TarskiGC β© TarskiGB) β
TarskiGC |
4 | 2, 3 | sstri 3953 |
. . . . 5
β’
((TarskiGC β© TarskiGB) β©
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) β
TarskiGC |
5 | 1, 4 | eqsstri 3978 |
. . . 4
β’ TarskiG
β TarskiGC |
6 | | axtrkg.g |
. . . 4
β’ (π β πΊ β TarskiG) |
7 | 5, 6 | sselid 3942 |
. . 3
β’ (π β πΊ β
TarskiGC) |
8 | | axtrkg.p |
. . . . . 6
β’ π = (BaseβπΊ) |
9 | | axtrkg.d |
. . . . . 6
β’ β =
(distβπΊ) |
10 | | axtrkg.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
11 | 8, 9, 10 | istrkgc 27396 |
. . . . 5
β’ (πΊ β TarskiGC
β (πΊ β V β§
(βπ₯ β π βπ¦ β π (π₯ β π¦) = (π¦ β π₯) β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β π¦) = (π§ β π§) β π₯ = π¦)))) |
12 | 11 | simprbi 497 |
. . . 4
β’ (πΊ β TarskiGC
β (βπ₯ β
π βπ¦ β π (π₯ β π¦) = (π¦ β π₯) β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β π¦) = (π§ β π§) β π₯ = π¦))) |
13 | 12 | simprd 496 |
. . 3
β’ (πΊ β TarskiGC
β βπ₯ β
π βπ¦ β π βπ§ β π ((π₯ β π¦) = (π§ β π§) β π₯ = π¦)) |
14 | 7, 13 | syl 17 |
. 2
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β π¦) = (π§ β π§) β π₯ = π¦)) |
15 | | axtgcgrid.4 |
. 2
β’ (π β (π β π) = (π β π)) |
16 | | axtgcgrid.1 |
. . 3
β’ (π β π β π) |
17 | | axtgcgrid.2 |
. . 3
β’ (π β π β π) |
18 | | axtgcgrid.3 |
. . 3
β’ (π β π β π) |
19 | | oveq1 7364 |
. . . . . 6
β’ (π₯ = π β (π₯ β π¦) = (π β π¦)) |
20 | 19 | eqeq1d 2738 |
. . . . 5
β’ (π₯ = π β ((π₯ β π¦) = (π§ β π§) β (π β π¦) = (π§ β π§))) |
21 | | eqeq1 2740 |
. . . . 5
β’ (π₯ = π β (π₯ = π¦ β π = π¦)) |
22 | 20, 21 | imbi12d 344 |
. . . 4
β’ (π₯ = π β (((π₯ β π¦) = (π§ β π§) β π₯ = π¦) β ((π β π¦) = (π§ β π§) β π = π¦))) |
23 | | oveq2 7365 |
. . . . . 6
β’ (π¦ = π β (π β π¦) = (π β π)) |
24 | 23 | eqeq1d 2738 |
. . . . 5
β’ (π¦ = π β ((π β π¦) = (π§ β π§) β (π β π) = (π§ β π§))) |
25 | | eqeq2 2748 |
. . . . 5
β’ (π¦ = π β (π = π¦ β π = π)) |
26 | 24, 25 | imbi12d 344 |
. . . 4
β’ (π¦ = π β (((π β π¦) = (π§ β π§) β π = π¦) β ((π β π) = (π§ β π§) β π = π))) |
27 | | id 22 |
. . . . . . 7
β’ (π§ = π β π§ = π) |
28 | 27, 27 | oveq12d 7375 |
. . . . . 6
β’ (π§ = π β (π§ β π§) = (π β π)) |
29 | 28 | eqeq2d 2747 |
. . . . 5
β’ (π§ = π β ((π β π) = (π§ β π§) β (π β π) = (π β π))) |
30 | 29 | imbi1d 341 |
. . . 4
β’ (π§ = π β (((π β π) = (π§ β π§) β π = π) β ((π β π) = (π β π) β π = π))) |
31 | 22, 26, 30 | rspc3v 3593 |
. . 3
β’ ((π β π β§ π β π β§ π β π) β (βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β π¦) = (π§ β π§) β π₯ = π¦) β ((π β π) = (π β π) β π = π))) |
32 | 16, 17, 18, 31 | syl3anc 1371 |
. 2
β’ (π β (βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β π¦) = (π§ β π§) β π₯ = π¦) β ((π β π) = (π β π) β π = π))) |
33 | 14, 15, 32 | mp2d 49 |
1
β’ (π β π = π) |