tglineineq

Description: Two distinct lines intersect in at most one point, variation. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019)

	Ref	Expression
Hypotheses	tglineintmo.p	$⊢ P = {Base}_{G}$
	tglineintmo.i	$⊢ I = Itv (G)$
	tglineintmo.l	$⊢ L = {Line}_{𝒢} (G)$
	tglineintmo.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglineintmo.a	$⊢ φ \to A \in ran L$
	tglineintmo.b	$⊢ φ \to B \in ran L$
	tglineintmo.c	$⊢ φ \to A \neq B$
	tglineineq.x	$⊢ φ \to X \in (A \cap B)$
	tglineineq.y	$⊢ φ \to Y \in (A \cap B)$
Assertion	tglineineq	$⊢ φ \to X = Y$

Proof

Step	Hyp	Ref	Expression
1		tglineintmo.p	$⊢ P = {Base}_{G}$
2		tglineintmo.i	$⊢ I = Itv (G)$
3		tglineintmo.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineintmo.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglineintmo.a	$⊢ φ \to A \in ran L$
6		tglineintmo.b	$⊢ φ \to B \in ran L$
7		tglineintmo.c	$⊢ φ \to A \neq B$
8		tglineineq.x	$⊢ φ \to X \in (A \cap B)$
9		tglineineq.y	$⊢ φ \to Y \in (A \cap B)$
10	1 2 3 4 5 6 7	tglineintmo	$⊢ φ \to \exists^{*} x (x \in A \land x \in B)$
11		elin	$⊢ X \in (A \cap B) \leftrightarrow (X \in A \land X \in B)$
12	8 11	sylib	$⊢ φ \to (X \in A \land X \in B)$
13		elin	$⊢ Y \in (A \cap B) \leftrightarrow (Y \in A \land Y \in B)$
14	9 13	sylib	$⊢ φ \to (Y \in A \land Y \in B)$
15		eleq1	$⊢ x = X \to (x \in A \leftrightarrow X \in A)$
16		eleq1	$⊢ x = X \to (x \in B \leftrightarrow X \in B)$
17	15 16	anbi12d	$⊢ x = X \to ((x \in A \land x \in B) \leftrightarrow (X \in A \land X \in B))$
18		eleq1	$⊢ x = Y \to (x \in A \leftrightarrow Y \in A)$
19		eleq1	$⊢ x = Y \to (x \in B \leftrightarrow Y \in B)$
20	18 19	anbi12d	$⊢ x = Y \to ((x \in A \land x \in B) \leftrightarrow (Y \in A \land Y \in B))$
21	17 20	moi	$⊢ ((X \in (A \cap B) \land Y \in (A \cap B)) \land \exists^{*} x (x \in A \land x \in B) \land ((X \in A \land X \in B) \land (Y \in A \land Y \in B))) \to X = Y$
22	8 9 10 12 14 21	syl212anc	$⊢ φ \to X = Y$

Metamath Proof Explorer

Theorem tglineineq

Proof