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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
	tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
Assertion	tglinethrueu	⊢ ( 𝜑 → ∃! 𝑥 ∈ 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	tghilberti1	⊢ ( 𝜑 → ∃ 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )
9	1 2 3 4 5 6 7	tghilberti2	⊢ ( 𝜑 → ∃* 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )
10		reu5	⊢ ( ∃! 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ↔ ( ∃ 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ∃* 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) )
11	8 9 10	sylanbrc	⊢ ( 𝜑 → ∃! 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )