| 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 | | inss2 4238 |
. . . . . 6
⊢
(TarskiGC ∩ TarskiGB) ⊆
TarskiGB |
| 4 | 2, 3 | sstri 3993 |
. . . . 5
⊢
((TarskiGC ∩ TarskiGB) ∩
(TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆
TarskiGB |
| 5 | 1, 4 | eqsstri 4030 |
. . . 4
⊢ TarskiG
⊆ TarskiGB |
| 6 | | axtrkg.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 7 | 5, 6 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝐺 ∈
TarskiGB) |
| 8 | | axtrkg.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
| 9 | | axtrkg.d |
. . . . . 6
⊢ − =
(dist‘𝐺) |
| 10 | | axtrkg.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
| 11 | 8, 9, 10 | istrkgb 28463 |
. . . . 5
⊢ (𝐺 ∈ TarskiGB
↔ (𝐺 ∈ V ∧
(∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎 ∈ 𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃∀𝑡 ∈ 𝒫 𝑃(∃𝑎 ∈ 𝑃 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏 ∈ 𝑃 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐼𝑦))))) |
| 12 | 11 | simprbi 496 |
. . . 4
⊢ (𝐺 ∈ TarskiGB
→ (∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎 ∈ 𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃∀𝑡 ∈ 𝒫 𝑃(∃𝑎 ∈ 𝑃 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏 ∈ 𝑃 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐼𝑦)))) |
| 13 | 12 | simp1d 1143 |
. . 3
⊢ (𝐺 ∈ TarskiGB
→ ∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦)) |
| 14 | 7, 13 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦)) |
| 15 | | axtgbtwnid.3 |
. 2
⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑋)) |
| 16 | | axtgbtwnid.1 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| 17 | | axtgbtwnid.2 |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
| 18 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
| 19 | 18, 18 | oveq12d 7449 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑥) = (𝑋𝐼𝑋)) |
| 20 | 19 | eleq2d 2827 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑥) ↔ 𝑦 ∈ (𝑋𝐼𝑋))) |
| 21 | | eqeq1 2741 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 = 𝑦 ↔ 𝑋 = 𝑦)) |
| 22 | 20, 21 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ↔ (𝑦 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑦))) |
| 23 | | eleq1 2829 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑋) ↔ 𝑌 ∈ (𝑋𝐼𝑋))) |
| 24 | | eqeq2 2749 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑋 = 𝑦 ↔ 𝑋 = 𝑌)) |
| 25 | 23, 24 | imbi12d 344 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑦) ↔ (𝑌 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑌))) |
| 26 | 22, 25 | rspc2v 3633 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) → (𝑌 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑌))) |
| 27 | 16, 17, 26 | syl2anc 584 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) → (𝑌 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑌))) |
| 28 | 14, 15, 27 | mp2d 49 |
1
⊢ (𝜑 → 𝑋 = 𝑌) |