tgsegconeu

Description: The point constructed in axtgsegcon is unique. (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	tkgeom.p	$⊢ P = {Base}_{G}$
	tkgeom.d	$⊢ \underset{˙}{-} = dist (G)$
	tkgeom.i	$⊢ I = Itv (G)$
	tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgsegconeu.x	$⊢ φ \to X \in P$
	tgsegconeu.y	$⊢ φ \to Y \in P$
	tgsegconeu.a	$⊢ φ \to A \in P$
	tgsegconeu.b	$⊢ φ \to B \in P$
	tgsegconeu.1	$⊢ φ \to X \neq Y$
Assertion	tgsegconeu	$⊢ φ \to \exists! z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B)$

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	$⊢ P = {Base}_{G}$
2		tkgeom.d	$⊢ \underset{˙}{-} = dist (G)$
3		tkgeom.i	$⊢ I = Itv (G)$
4		tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgsegconeu.x	$⊢ φ \to X \in P$
6		tgsegconeu.y	$⊢ φ \to Y \in P$
7		tgsegconeu.a	$⊢ φ \to A \in P$
8		tgsegconeu.b	$⊢ φ \to B \in P$
9		tgsegconeu.1	$⊢ φ \to X \neq Y$
10	1 2 3 4 5 6 7 8	axtgsegcon	$⊢ φ \to \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B)$
11	4	ad6antr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to G \in 𝒢_{Tarski}$
12	6	ad6antr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to Y \in P$
13	7	ad6antr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to A \in P$
14	8	ad6antr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to B \in P$
15	5	ad6antr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to X \in P$
16		simp-6r	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to z \in P$
17		simp-5r	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to s \in P$
18	9	ad6antr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to X \neq Y$
19		simplr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to Y \in (X I z)$
20		simpllr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to Y \in (X I s)$
21		simpr	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to Y \underset{˙}{-} z = A \underset{˙}{-} B$
22		simp-4r	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to Y \underset{˙}{-} s = A \underset{˙}{-} B$
23	1 2 3 11 12 13 14 15 16 17 18 19 20 21 22	tgsegconeq	$⊢ ((((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land Y \in (X I z)) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \to z = s$
24	23	anasss	$⊢ (((((φ \land z \in P) \land s \in P) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \land Y \in (X I s)) \land (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B)) \to z = s$
25	24	an42ds	$⊢ (((((φ \land z \in P) \land s \in P) \land (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B)) \land Y \in (X I s)) \land Y \underset{˙}{-} s = A \underset{˙}{-} B) \to z = s$
26	25	anasss	$⊢ ((((φ \land z \in P) \land s \in P) \land (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B)) \land (Y \in (X I s) \land Y \underset{˙}{-} s = A \underset{˙}{-} B)) \to z = s$
27	26	expl	$⊢ ((φ \land z \in P) \land s \in P) \to (((Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \land (Y \in (X I s) \land Y \underset{˙}{-} s = A \underset{˙}{-} B)) \to z = s)$
28	27	anasss	$⊢ (φ \land (z \in P \land s \in P)) \to (((Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \land (Y \in (X I s) \land Y \underset{˙}{-} s = A \underset{˙}{-} B)) \to z = s)$
29	28	ralrimivva	$⊢ φ \to \forall z \in P \forall s \in P (((Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \land (Y \in (X I s) \land Y \underset{˙}{-} s = A \underset{˙}{-} B)) \to z = s)$
30		oveq2	$⊢ z = s \to X I z = X I s$
31	30	eleq2d	$⊢ z = s \to (Y \in (X I z) \leftrightarrow Y \in (X I s))$
32		oveq2	$⊢ z = s \to Y \underset{˙}{-} z = Y \underset{˙}{-} s$
33	32	eqeq1d	$⊢ z = s \to (Y \underset{˙}{-} z = A \underset{˙}{-} B \leftrightarrow Y \underset{˙}{-} s = A \underset{˙}{-} B)$
34	31 33	anbi12d	$⊢ z = s \to ((Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \leftrightarrow (Y \in (X I s) \land Y \underset{˙}{-} s = A \underset{˙}{-} B))$
35	34	reu4	$⊢ \exists! z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \leftrightarrow (\exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \land \forall z \in P \forall s \in P (((Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B) \land (Y \in (X I s) \land Y \underset{˙}{-} s = A \underset{˙}{-} B)) \to z = s))$
36	10 29 35	sylanbrc	$⊢ φ \to \exists! z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B)$

Metamath Proof Explorer

Theorem tgsegconeu

Proof