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 ) )