Metamath Proof Explorer

Theorem hilbert1.2

Description: There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by NM, 17-Jun-2017)

Ref Expression
Assertion hilbert1.2 
|- ( P =/= Q -> E* x e. LinesEE ( P e. x /\ Q e. x ) )

Proof

Step Hyp Ref Expression
1 an4 
 |-  ( ( ( x e. LinesEE /\ y e. LinesEE ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) <-> ( ( x e. LinesEE /\ ( P e. x /\ Q e. x ) ) /\ ( y e. LinesEE /\ ( P e. y /\ Q e. y ) ) ) )
2 simprl 
 |-  ( ( P =/= Q /\ ( x e. LinesEE /\ ( P e. x /\ Q e. x ) ) ) -> x e. LinesEE )
3 simprr 
 |-  ( ( P =/= Q /\ ( x e. LinesEE /\ ( P e. x /\ Q e. x ) ) ) -> ( P e. x /\ Q e. x ) )
4 simpl 
 |-  ( ( P =/= Q /\ ( x e. LinesEE /\ ( P e. x /\ Q e. x ) ) ) -> P =/= Q )
5 linethru 
 |-  ( ( x e. LinesEE /\ ( P e. x /\ Q e. x ) /\ P =/= Q ) -> x = ( P Line Q ) )
6 2 3 4 5 syl3anc 
 |-  ( ( P =/= Q /\ ( x e. LinesEE /\ ( P e. x /\ Q e. x ) ) ) -> x = ( P Line Q ) )
7 6 ex 
 |-  ( P =/= Q -> ( ( x e. LinesEE /\ ( P e. x /\ Q e. x ) ) -> x = ( P Line Q ) ) )
8 simprl 
 |-  ( ( P =/= Q /\ ( y e. LinesEE /\ ( P e. y /\ Q e. y ) ) ) -> y e. LinesEE )
9 simprr 
 |-  ( ( P =/= Q /\ ( y e. LinesEE /\ ( P e. y /\ Q e. y ) ) ) -> ( P e. y /\ Q e. y ) )
10 simpl 
 |-  ( ( P =/= Q /\ ( y e. LinesEE /\ ( P e. y /\ Q e. y ) ) ) -> P =/= Q )
11 linethru 
 |-  ( ( y e. LinesEE /\ ( P e. y /\ Q e. y ) /\ P =/= Q ) -> y = ( P Line Q ) )
12 8 9 10 11 syl3anc 
 |-  ( ( P =/= Q /\ ( y e. LinesEE /\ ( P e. y /\ Q e. y ) ) ) -> y = ( P Line Q ) )
13 12 ex 
 |-  ( P =/= Q -> ( ( y e. LinesEE /\ ( P e. y /\ Q e. y ) ) -> y = ( P Line Q ) ) )
14 7 13 anim12d 
 |-  ( P =/= Q -> ( ( ( x e. LinesEE /\ ( P e. x /\ Q e. x ) ) /\ ( y e. LinesEE /\ ( P e. y /\ Q e. y ) ) ) -> ( x = ( P Line Q ) /\ y = ( P Line Q ) ) ) )
15 eqtr3 
 |-  ( ( x = ( P Line Q ) /\ y = ( P Line Q ) ) -> x = y )
16 14 15 syl6 
 |-  ( P =/= Q -> ( ( ( x e. LinesEE /\ ( P e. x /\ Q e. x ) ) /\ ( y e. LinesEE /\ ( P e. y /\ Q e. y ) ) ) -> x = y ) )
17 1 16 syl5bi 
 |-  ( P =/= Q -> ( ( ( x e. LinesEE /\ y e. LinesEE ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> x = y ) )
18 17 expd 
 |-  ( P =/= Q -> ( ( x e. LinesEE /\ y e. LinesEE ) -> ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) ) )
19 18 ralrimivv 
 |-  ( P =/= Q -> A. x e. LinesEE A. y e. LinesEE ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) )
20 eleq2w 
 |-  ( x = y -> ( P e. x <-> P e. y ) )
21 eleq2w 
 |-  ( x = y -> ( Q e. x <-> Q e. y ) )
22 20 21 anbi12d 
 |-  ( x = y -> ( ( P e. x /\ Q e. x ) <-> ( P e. y /\ Q e. y ) ) )
23 22 rmo4 
 |-  ( E* x e. LinesEE ( P e. x /\ Q e. x ) <-> A. x e. LinesEE A. y e. LinesEE ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) )
24 19 23 sylibr 
 |-  ( P =/= Q -> E* x e. LinesEE ( P e. x /\ Q e. x ) )