Metamath Proof Explorer

Theorem eulplig

Description: Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021)

Ref Expression
Hypothesis eulplig.1 
|- P = U. G
Assertion eulplig 
|- ( ( G e. Plig /\ ( ( A e. P /\ B e. P ) /\ A =/= B ) ) -> E! l e. G ( A e. l /\ B e. l ) )

Proof

Step Hyp Ref Expression
1 eulplig.1 
 |-  P = U. G
2 1 isplig 
 |-  ( G e. Plig -> ( G e. Plig <-> ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) /\ A. l e. G E. a e. P E. b e. P ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. P E. b e. P E. c e. P A. l e. G -. ( a e. l /\ b e. l /\ c e. l ) ) ) )
3 2 ibi 
 |-  ( G e. Plig -> ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) /\ A. l e. G E. a e. P E. b e. P ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. P E. b e. P E. c e. P A. l e. G -. ( a e. l /\ b e. l /\ c e. l ) ) )
4 simp1 
 |-  ( ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) /\ A. l e. G E. a e. P E. b e. P ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. P E. b e. P E. c e. P A. l e. G -. ( a e. l /\ b e. l /\ c e. l ) ) -> A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) )
5 simpl 
 |-  ( ( a = A /\ b = B ) -> a = A )
6 simpr 
 |-  ( ( a = A /\ b = B ) -> b = B )
7 5 6 neeq12d 
 |-  ( ( a = A /\ b = B ) -> ( a =/= b <-> A =/= B ) )
8 eleq1 
 |-  ( a = A -> ( a e. l <-> A e. l ) )
9 eleq1 
 |-  ( b = B -> ( b e. l <-> B e. l ) )
10 8 9 bi2anan9 
 |-  ( ( a = A /\ b = B ) -> ( ( a e. l /\ b e. l ) <-> ( A e. l /\ B e. l ) ) )
11 10 reubidv 
 |-  ( ( a = A /\ b = B ) -> ( E! l e. G ( a e. l /\ b e. l ) <-> E! l e. G ( A e. l /\ B e. l ) ) )
12 7 11 imbi12d 
 |-  ( ( a = A /\ b = B ) -> ( ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) <-> ( A =/= B -> E! l e. G ( A e. l /\ B e. l ) ) ) )
13 12 rspc2gv 
 |-  ( ( A e. P /\ B e. P ) -> ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) -> ( A =/= B -> E! l e. G ( A e. l /\ B e. l ) ) ) )
14 13 com23 
 |-  ( ( A e. P /\ B e. P ) -> ( A =/= B -> ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) -> E! l e. G ( A e. l /\ B e. l ) ) ) )
15 14 imp 
 |-  ( ( ( A e. P /\ B e. P ) /\ A =/= B ) -> ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) -> E! l e. G ( A e. l /\ B e. l ) ) )
16 15 com12 
 |-  ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) -> ( ( ( A e. P /\ B e. P ) /\ A =/= B ) -> E! l e. G ( A e. l /\ B e. l ) ) )
17 3 4 16 3syl 
 |-  ( G e. Plig -> ( ( ( A e. P /\ B e. P ) /\ A =/= B ) -> E! l e. G ( A e. l /\ B e. l ) ) )
18 17 imp 
 |-  ( ( G e. Plig /\ ( ( A e. P /\ B e. P ) /\ A =/= B ) ) -> E! l e. G ( A e. l /\ B e. l ) )