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