Metamath Proof Explorer

Theorem tglinethrueu

Description: There is a unique line going through any two distinct points. Theorem 6.19 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 25-May-2019)

		Ref	Expression
	Hypotheses	tglineelsb2.p	$⊢ B = {Base}_{G}$
		tglineelsb2.i	$⊢ I = Itv (G)$
		tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
		tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		tglineelsb2.1	$⊢ φ \to P \in B$
		tglineelsb2.2	$⊢ φ \to Q \in B$
		tglineelsb2.4	$⊢ φ \to P \neq Q$
	Assertion	tglinethrueu	$⊢ φ \to \exists! x \in ran L (P \in x \land Q \in x)$

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	$⊢ B = {Base}_{G}$
2		tglineelsb2.i	$⊢ I = Itv (G)$
3		tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglineelsb2.1	$⊢ φ \to P \in B$
6		tglineelsb2.2	$⊢ φ \to Q \in B$
7		tglineelsb2.4	$⊢ φ \to P \neq Q$
8	1 2 3 4 5 6 7	tghilberti1	$⊢ φ \to \exists x \in ran L (P \in x \land Q \in x)$
9	1 2 3 4 5 6 7	tghilberti2	$⊢ φ \to \exists^{*} x \in ran L (P \in x \land Q \in x)$
10		reu5	$⊢ \exists! x \in ran L (P \in x \land Q \in x) \leftrightarrow (\exists x \in ran L (P \in x \land Q \in x) \land \exists^{*} x \in ran L (P \in x \land Q \in x))$
11	8 9 10	sylanbrc	$⊢ φ \to \exists! x \in ran L (P \in x \land Q \in x)$