Metamath Proof Explorer


Theorem tghilberti2

Description: There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (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 tghilberti2 φ * 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 4 3ad2ant1 φ x ran L y ran L P x Q x P y Q y G 𝒢 Tarski
9 5 3ad2ant1 φ x ran L y ran L P x Q x P y Q y P B
10 6 3ad2ant1 φ x ran L y ran L P x Q x P y Q y Q B
11 7 3ad2ant1 φ x ran L y ran L P x Q x P y Q y P Q
12 simp2l φ x ran L y ran L P x Q x P y Q y x ran L
13 simp3ll φ x ran L y ran L P x Q x P y Q y P x
14 simp3lr φ x ran L y ran L P x Q x P y Q y Q x
15 1 2 3 8 9 10 11 11 12 13 14 tglinethru φ x ran L y ran L P x Q x P y Q y x = P L Q
16 simp2r φ x ran L y ran L P x Q x P y Q y y ran L
17 simp3rl φ x ran L y ran L P x Q x P y Q y P y
18 simp3rr φ x ran L y ran L P x Q x P y Q y Q y
19 1 2 3 8 9 10 11 11 16 17 18 tglinethru φ x ran L y ran L P x Q x P y Q y y = P L Q
20 15 19 eqtr4d φ x ran L y ran L P x Q x P y Q y x = y
21 20 3expia φ x ran L y ran L P x Q x P y Q y x = y
22 21 ralrimivva φ x ran L y ran L P x Q x P y Q y x = y
23 eleq2w x = y P x P y
24 eleq2w x = y Q x Q y
25 23 24 anbi12d x = y P x Q x P y Q y
26 25 rmo4 * x ran L P x Q x x ran L y ran L P x Q x P y Q y x = y
27 22 26 sylibr φ * x ran L P x Q x