| Step | Hyp | Ref
| Expression |
| 1 | | df-trkg 28461 |
. . . . 5
⊢ TarskiG =
((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB
∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
| 2 | | inss1 4237 |
. . . . . 6
⊢
((TarskiGC ∩ TarskiGB) ∩
(TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩
TarskiGB) |
| 3 | | inss1 4237 |
. . . . . 6
⊢
(TarskiGC ∩ TarskiGB) ⊆
TarskiGC |
| 4 | 2, 3 | sstri 3993 |
. . . . 5
⊢
((TarskiGC ∩ TarskiGB) ∩
(TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆
TarskiGC |
| 5 | 1, 4 | eqsstri 4030 |
. . . 4
⊢ TarskiG
⊆ TarskiGC |
| 6 | | axtrkg.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 7 | 5, 6 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝐺 ∈
TarskiGC) |
| 8 | | axtrkg.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
| 9 | | axtrkg.d |
. . . . . 6
⊢ − =
(dist‘𝐺) |
| 10 | | axtrkg.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
| 11 | 8, 9, 10 | istrkgc 28462 |
. . . . 5
⊢ (𝐺 ∈ TarskiGC
↔ (𝐺 ∈ V ∧
(∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦)))) |
| 12 | 11 | simprbi 496 |
. . . 4
⊢ (𝐺 ∈ TarskiGC
→ (∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦))) |
| 13 | 12 | simpld 494 |
. . 3
⊢ (𝐺 ∈ TarskiGC
→ ∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥)) |
| 14 | 7, 13 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥)) |
| 15 | | axtgcgrrflx.1 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| 16 | | axtgcgrrflx.2 |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
| 17 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦)) |
| 18 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑦 − 𝑥) = (𝑦 − 𝑋)) |
| 19 | 17, 18 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑦 − 𝑥) ↔ (𝑋 − 𝑦) = (𝑦 − 𝑋))) |
| 20 | | oveq2 7439 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌)) |
| 21 | | oveq1 7438 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑦 − 𝑋) = (𝑌 − 𝑋)) |
| 22 | 20, 21 | eqeq12d 2753 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑦 − 𝑋) ↔ (𝑋 − 𝑌) = (𝑌 − 𝑋))) |
| 23 | 19, 22 | rspc2v 3633 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) → (𝑋 − 𝑌) = (𝑌 − 𝑋))) |
| 24 | 15, 16, 23 | syl2anc 584 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) → (𝑋 − 𝑌) = (𝑌 − 𝑋))) |
| 25 | 14, 24 | mpd 15 |
1
⊢ (𝜑 → (𝑋 − 𝑌) = (𝑌 − 𝑋)) |