Step | Hyp | Ref
| Expression |
1 | | df-trkg 26544 |
. . . . 5
⊢ TarskiG =
((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB
∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
2 | | inss1 4143 |
. . . . . 6
⊢
((TarskiGC ∩ TarskiGB) ∩
(TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩
TarskiGB) |
3 | | inss1 4143 |
. . . . . 6
⊢
(TarskiGC ∩ TarskiGB) ⊆
TarskiGC |
4 | 2, 3 | sstri 3910 |
. . . . 5
⊢
((TarskiGC ∩ TarskiGB) ∩
(TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆
TarskiGC |
5 | 1, 4 | eqsstri 3935 |
. . . 4
⊢ TarskiG
⊆ TarskiGC |
6 | | axtrkg.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
7 | 5, 6 | sseldi 3899 |
. . 3
⊢ (𝜑 → 𝐺 ∈
TarskiGC) |
8 | | axtrkg.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
9 | | axtrkg.d |
. . . . . 6
⊢ − =
(dist‘𝐺) |
10 | | axtrkg.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
11 | 8, 9, 10 | istrkgc 26545 |
. . . . 5
⊢ (𝐺 ∈ TarskiGC
↔ (𝐺 ∈ V ∧
(∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦)))) |
12 | 11 | simprbi 500 |
. . . 4
⊢ (𝐺 ∈ TarskiGC
→ (∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦))) |
13 | 12 | simpld 498 |
. . 3
⊢ (𝐺 ∈ TarskiGC
→ ∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥)) |
14 | 7, 13 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥)) |
15 | | axtgcgrrflx.1 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
16 | | axtgcgrrflx.2 |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
17 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦)) |
18 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑦 − 𝑥) = (𝑦 − 𝑋)) |
19 | 17, 18 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑦 − 𝑥) ↔ (𝑋 − 𝑦) = (𝑦 − 𝑋))) |
20 | | oveq2 7221 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌)) |
21 | | oveq1 7220 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑦 − 𝑋) = (𝑌 − 𝑋)) |
22 | 20, 21 | eqeq12d 2753 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑦 − 𝑋) ↔ (𝑋 − 𝑌) = (𝑌 − 𝑋))) |
23 | 19, 22 | rspc2v 3547 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) → (𝑋 − 𝑌) = (𝑌 − 𝑋))) |
24 | 15, 16, 23 | syl2anc 587 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) → (𝑋 − 𝑌) = (𝑌 − 𝑋))) |
25 | 14, 24 | mpd 15 |
1
⊢ (𝜑 → (𝑋 − 𝑌) = (𝑌 − 𝑋)) |