Theorem linethrueu

Description: There is a unique line going through any two distinct points. Theorem 6.19 of Schwabhauser p. 46. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	linethrueu	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ∃! 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		hilbert1.1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ∃ 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )
2		simpr3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 ≠ 𝑄 )
3		hilbert1.2	⊢ ( 𝑃 ≠ 𝑄 → ∃* 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )
4	2 3	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ∃* 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )
5		reu5	⊢ ( ∃! 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ↔ ( ∃ 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ∃* 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ) )
6	1 4 5	sylanbrc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ∃! 𝑥 ∈ LinesEE ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )