tghilberti1

Description: There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (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	tghilberti1	$⊢ φ \to \exists x \in ran L (P \in x \land Q \in x)$

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	tgelrnln	$⊢ φ \to P L Q \in ran L$
9	1 2 3 4 5 6 7	tglinerflx1	$⊢ φ \to P \in (P L Q)$
10	1 2 3 4 5 6 7	tglinerflx2	$⊢ φ \to Q \in (P L Q)$
11		eleq2	$⊢ x = P L Q \to (P \in x \leftrightarrow P \in (P L Q))$
12		eleq2	$⊢ x = P L Q \to (Q \in x \leftrightarrow Q \in (P L Q))$
13	11 12	anbi12d	$⊢ x = P L Q \to ((P \in x \land Q \in x) \leftrightarrow (P \in (P L Q) \land Q \in (P L Q)))$
14	13	rspcev	$⊢ (P L Q \in ran L \land (P \in (P L Q) \land Q \in (P L Q))) \to \exists x \in ran L (P \in x \land Q \in x)$
15	8 9 10 14	syl12anc	$⊢ φ \to \exists x \in ran L (P \in x \land Q \in x)$

Metamath Proof Explorer