Metamath Proof Explorer

Theorem tglineinsn

Description: If two distinct lines intersect, it is at a single point. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 17-Jun-2026)

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

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		tglineinsn.a	$⊢ φ \to A \in ran L$
6		tglineinsn.b	$⊢ φ \to B \in ran L$
7		tglineinsn.c	$⊢ φ \to A \neq B$
8		tglineinsn.x	$⊢ φ \to X \in (A \cap B)$
9	4	adantr	$⊢ (φ \land x \in (A \cap B)) \to G \in 𝒢_{Tarski}$
10	5	adantr	$⊢ (φ \land x \in (A \cap B)) \to A \in ran L$
11	6	adantr	$⊢ (φ \land x \in (A \cap B)) \to B \in ran L$
12	7	adantr	$⊢ (φ \land x \in (A \cap B)) \to A \neq B$
13		simpr	$⊢ (φ \land x \in (A \cap B)) \to x \in (A \cap B)$
14	8	adantr	$⊢ (φ \land x \in (A \cap B)) \to X \in (A \cap B)$
15	1 2 3 9 10 11 12 13 14	tglineineq	$⊢ (φ \land x \in (A \cap B)) \to x = X$
16	15 8	eqsnd	$⊢ φ \to A \cap B = \{X\}$