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 ⊢ φ → G ∈ 𝒢 Tarski
tglineelsb2.1 ⊢ φ → P ∈ B
tglineelsb2.2 ⊢ φ → Q ∈ B
tglineelsb2.4 ⊢ φ → P ≠ Q
Assertion tglinethrueu ⊢ φ → ∃! x ∈ ran ⁡ L P ∈ x ∧ Q ∈ 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 ⊢ φ → G ∈ 𝒢 Tarski
5 tglineelsb2.1 ⊢ φ → P ∈ B
6 tglineelsb2.2 ⊢ φ → Q ∈ B
7 tglineelsb2.4 ⊢ φ → P ≠ Q
8 1 2 3 4 5 6 7 tghilberti1 ⊢ φ → ∃ x ∈ ran ⁡ L P ∈ x ∧ Q ∈ x
9 1 2 3 4 5 6 7 tghilberti2 ⊢ φ → ∃* x ∈ ran ⁡ L P ∈ x ∧ Q ∈ x
10 reu5 ⊢ ∃! x ∈ ran ⁡ L P ∈ x ∧ Q ∈ x ↔ ∃ x ∈ ran ⁡ L P ∈ x ∧ Q ∈ x ∧ ∃* x ∈ ran ⁡ L P ∈ x ∧ Q ∈ x
11 8 9 10 sylanbrc ⊢ φ → ∃! x ∈ ran ⁡ L P ∈ x ∧ Q ∈ x