Metamath Proof Explorer

Theorem axtgbtwnid

Description: Identity of Betweenness. Axiom A6 of Schwabhauser p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Hypotheses axtrkg.p ⊢P=BaseG
axtrkg.d ⊢-˙=dist⁡G
axtrkg.i ⊢I=Itv⁡G
axtrkg.g ⊢φ→G∈𝒢Tarski
axtgbtwnid.1 ⊢φ→X∈P
axtgbtwnid.2 ⊢φ→Y∈P
axtgbtwnid.3 ⊢φ→Y∈XIX
Assertion axtgbtwnid ⊢φ→X=Y

Proof

Step Hyp Ref Expression
1 axtrkg.p ⊢P=BaseG
2 axtrkg.d ⊢-˙=dist⁡G
3 axtrkg.i ⊢I=Itv⁡G
4 axtrkg.g ⊢φ→G∈𝒢Tarski
5 axtgbtwnid.1 ⊢φ→X∈P
6 axtgbtwnid.2 ⊢φ→Y∈P
7 axtgbtwnid.3 ⊢φ→Y∈XIX
8 df-trkg ⊢𝒢Tarski=𝒢TarskiC∩𝒢TarskiB∩𝒢TarskiCB∩f|[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz
9 inss1 ⊢𝒢TarskiC∩𝒢TarskiB∩𝒢TarskiCB∩f|[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz⊆𝒢TarskiC∩𝒢TarskiB
10 inss2 ⊢𝒢TarskiC∩𝒢TarskiB⊆𝒢TarskiB
11 9 10 sstri ⊢𝒢TarskiC∩𝒢TarskiB∩𝒢TarskiCB∩f|[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz⊆𝒢TarskiB
12 8 11 eqsstri ⊢𝒢Tarski⊆𝒢TarskiB
13 12 4 sselid ⊢φ→G∈𝒢TarskiB
14 1 2 3 istrkgb ⊢G∈𝒢TarskiB↔G∈V∧∀x∈P∀y∈Py∈xIx→x=y∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx∧∀s∈𝒫P∀t∈𝒫P∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy
15 14 simprbi ⊢G∈𝒢TarskiB→∀x∈P∀y∈Py∈xIx→x=y∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx∧∀s∈𝒫P∀t∈𝒫P∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy
16 15 simp1d ⊢G∈𝒢TarskiB→∀x∈P∀y∈Py∈xIx→x=y
17 13 16 syl ⊢φ→∀x∈P∀y∈Py∈xIx→x=y
18 id ⊢x=X→x=X
19 18 18 oveq12d ⊢x=X→xIx=XIX
20 19 eleq2d ⊢x=X→y∈xIx↔y∈XIX
21 eqeq1 ⊢x=X→x=y↔X=y
22 20 21 imbi12d ⊢x=X→y∈xIx→x=y↔y∈XIX→X=y
23 eleq1 ⊢y=Y→y∈XIX↔Y∈XIX
24 eqeq2 ⊢y=Y→X=y↔X=Y
25 23 24 imbi12d ⊢y=Y→y∈XIX→X=y↔Y∈XIX→X=Y
26 22 25 rspc2v ⊢X∈P∧Y∈P→∀x∈P∀y∈Py∈xIx→x=y→Y∈XIX→X=Y
27 5 6 26 syl2anc ⊢φ→∀x∈P∀y∈Py∈xIx→x=y→Y∈XIX→X=Y
28 17 7 27 mp2d ⊢φ→X=Y