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 = ( LineG ` G )
tglineelsb2.g
|- ( ph -> G e. TarskiG )
tglineelsb2.1
|- ( ph -> P e. B )
tglineelsb2.2
|- ( ph -> Q e. B )
tglineelsb2.4
|- ( ph -> P =/= Q )
Assertion tghilberti2
|- ( ph -> E* x e. ran L ( P e. x /\ Q e. x ) )

Proof

Step Hyp Ref Expression
1 tglineelsb2.p
 |-  B = ( Base ` G )
2 tglineelsb2.i
 |-  I = ( Itv ` G )
3 tglineelsb2.l
 |-  L = ( LineG ` G )
4 tglineelsb2.g
 |-  ( ph -> G e. TarskiG )
5 tglineelsb2.1
 |-  ( ph -> P e. B )
6 tglineelsb2.2
 |-  ( ph -> Q e. B )
7 tglineelsb2.4
 |-  ( ph -> P =/= Q )
8 4 3ad2ant1
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> G e. TarskiG )
9 5 3ad2ant1
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> P e. B )
10 6 3ad2ant1
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> Q e. B )
11 7 3ad2ant1
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> P =/= Q )
12 simp2l
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> x e. ran L )
13 simp3ll
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> P e. x )
14 simp3lr
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> Q e. x )
15 1 2 3 8 9 10 11 11 12 13 14 tglinethru
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> x = ( P L Q ) )
16 simp2r
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> y e. ran L )
17 simp3rl
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> P e. y )
18 simp3rr
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> Q e. y )
19 1 2 3 8 9 10 11 11 16 17 18 tglinethru
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> y = ( P L Q ) )
20 15 19 eqtr4d
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> x = y )
21 20 3expia
 |-  ( ( ph /\ ( x e. ran L /\ y e. ran L ) ) -> ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) )
22 21 ralrimivva
 |-  ( ph -> A. x e. ran L A. y e. ran L ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) )
23 eleq2w
 |-  ( x = y -> ( P e. x <-> P e. y ) )
24 eleq2w
 |-  ( x = y -> ( Q e. x <-> Q e. y ) )
25 23 24 anbi12d
 |-  ( x = y -> ( ( P e. x /\ Q e. x ) <-> ( P e. y /\ Q e. y ) ) )
26 25 rmo4
 |-  ( E* x e. ran L ( P e. x /\ Q e. x ) <-> A. x e. ran L A. y e. ran L ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) )
27 22 26 sylibr
 |-  ( ph -> E* x e. ran L ( P e. x /\ Q e. x ) )