axtgbtwnid

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

	Ref	Expression
Hypotheses	axtrkg.p	$⊢ P = {Base}_{G}$
	axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
	axtrkg.i	$⊢ I = Itv (G)$
	axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	axtgbtwnid.1	$⊢ φ \to X \in P$
	axtgbtwnid.2	$⊢ φ \to Y \in P$
	axtgbtwnid.3	$⊢ φ \to Y \in (X I X)$
Assertion	axtgbtwnid	$⊢ φ \to X = Y$

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	$⊢ P = {Base}_{G}$
2		axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		axtrkg.i	$⊢ I = Itv (G)$
4		axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		axtgbtwnid.1	$⊢ φ \to X \in P$
6		axtgbtwnid.2	$⊢ φ \to Y \in P$
7		axtgbtwnid.3	$⊢ φ \to Y \in (X I X)$
8		df-trkg	$⊢ 𝒢_{Tarski} = (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
9		inss1	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}$
10		inss2	$⊢ 𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B} \subseteq 𝒢_{Tarski}^{B}$
11	9 10	sstri	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{B}$
12	8 11	eqsstri	$⊢ 𝒢_{Tarski} \subseteq 𝒢_{Tarski}^{B}$
13	12 4	sselid	$⊢ φ \to G \in 𝒢_{Tarski}^{B}$
14	1 2 3	istrkgb	$⊢ G \in 𝒢_{Tarski}^{B} \leftrightarrow (G \in V \land (\forall x \in P \forall y \in P (y \in (x I x) \to x = y) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \land \forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y))))$
15	14	simprbi	$⊢ G \in 𝒢_{Tarski}^{B} \to (\forall x \in P \forall y \in P (y \in (x I x) \to x = y) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \land \forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y)))$
16	15	simp1d	$⊢ G \in 𝒢_{Tarski}^{B} \to \forall x \in P \forall y \in P (y \in (x I x) \to x = y)$
17	13 16	syl	$⊢ φ \to \forall x \in P \forall y \in P (y \in (x I x) \to x = y)$
18		id	$⊢ x = X \to x = X$
19	18 18	oveq12d	$⊢ x = X \to x I x = X I X$
20	19	eleq2d	$⊢ x = X \to (y \in (x I x) \leftrightarrow y \in (X I X))$
21		eqeq1	$⊢ x = X \to (x = y \leftrightarrow X = y)$
22	20 21	imbi12d	$⊢ x = X \to ((y \in (x I x) \to x = y) \leftrightarrow (y \in (X I X) \to X = y))$
23		eleq1	$⊢ y = Y \to (y \in (X I X) \leftrightarrow Y \in (X I X))$
24		eqeq2	$⊢ y = Y \to (X = y \leftrightarrow X = Y)$
25	23 24	imbi12d	$⊢ y = Y \to ((y \in (X I X) \to X = y) \leftrightarrow (Y \in (X I X) \to X = Y))$
26	22 25	rspc2v	$⊢ (X \in P \land Y \in P) \to (\forall x \in P \forall y \in P (y \in (x I x) \to x = y) \to (Y \in (X I X) \to X = Y))$
27	5 6 26	syl2anc	$⊢ φ \to (\forall x \in P \forall y \in P (y \in (x I x) \to x = y) \to (Y \in (X I X) \to X = Y))$
28	17 7 27	mp2d	$⊢ φ \to X = Y$

Metamath Proof Explorer

Theorem axtgbtwnid

Proof