Theorem 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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
	tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
Assertion	tghilberti1	⊢ ( 𝜑 → ∃ 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6		tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
7		tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
8	1 2 3 4 5 6 7	tgelrnln	⊢ ( 𝜑 → ( 𝑃 𝐿 𝑄 ) ∈ ran 𝐿 )
9	1 2 3 4 5 6 7	tglinerflx1	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑃 𝐿 𝑄 ) )
10	1 2 3 4 5 6 7	tglinerflx2	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 𝐿 𝑄 ) )
11		eleq2	⊢ ( 𝑥 = ( 𝑃 𝐿 𝑄 ) → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ ( 𝑃 𝐿 𝑄 ) ) )
12		eleq2	⊢ ( 𝑥 = ( 𝑃 𝐿 𝑄 ) → ( 𝑄 ∈ 𝑥 ↔ 𝑄 ∈ ( 𝑃 𝐿 𝑄 ) ) )
13	11 12	anbi12d	⊢ ( 𝑥 = ( 𝑃 𝐿 𝑄 ) → ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ↔ ( 𝑃 ∈ ( 𝑃 𝐿 𝑄 ) ∧ 𝑄 ∈ ( 𝑃 𝐿 𝑄 ) ) ) )
14	13	rspcev	⊢ ( ( ( 𝑃 𝐿 𝑄 ) ∈ ran 𝐿 ∧ ( 𝑃 ∈ ( 𝑃 𝐿 𝑄 ) ∧ 𝑄 ∈ ( 𝑃 𝐿 𝑄 ) ) ) → ∃ 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )
15	8 9 10 14	syl12anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )