Metamath Proof Explorer

Theorem lpni

Description: For any line in a planar incidence geometry, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009)

Ref Expression
Hypothesis l2p.1 
|- P = U. G
Assertion lpni 
|- ( ( G e. Plig /\ L e. G ) -> E. a e. P a e/ L )

Proof

Step Hyp Ref Expression
1 l2p.1 
 |-  P = U. G
2 1 tncp 
 |-  ( G e. Plig -> E. b e. P E. c e. P E. d e. P A. l e. G -. ( b e. l /\ c e. l /\ d e. l ) )
3 eleq2 
 |-  ( l = L -> ( b e. l <-> b e. L ) )
4 eleq2 
 |-  ( l = L -> ( c e. l <-> c e. L ) )
5 eleq2 
 |-  ( l = L -> ( d e. l <-> d e. L ) )
6 3 4 5 3anbi123d 
 |-  ( l = L -> ( ( b e. l /\ c e. l /\ d e. l ) <-> ( b e. L /\ c e. L /\ d e. L ) ) )
7 6 notbid 
 |-  ( l = L -> ( -. ( b e. l /\ c e. l /\ d e. l ) <-> -. ( b e. L /\ c e. L /\ d e. L ) ) )
8 7 rspccv 
 |-  ( A. l e. G -. ( b e. l /\ c e. l /\ d e. l ) -> ( L e. G -> -. ( b e. L /\ c e. L /\ d e. L ) ) )
9 eleq1w 
 |-  ( a = b -> ( a e. L <-> b e. L ) )
10 9 notbid 
 |-  ( a = b -> ( -. a e. L <-> -. b e. L ) )
11 10 rspcev 
 |-  ( ( b e. P /\ -. b e. L ) -> E. a e. P -. a e. L )
12 11 ex 
 |-  ( b e. P -> ( -. b e. L -> E. a e. P -. a e. L ) )
13 eleq1w 
 |-  ( a = c -> ( a e. L <-> c e. L ) )
14 13 notbid 
 |-  ( a = c -> ( -. a e. L <-> -. c e. L ) )
15 14 rspcev 
 |-  ( ( c e. P /\ -. c e. L ) -> E. a e. P -. a e. L )
16 15 ex 
 |-  ( c e. P -> ( -. c e. L -> E. a e. P -. a e. L ) )
17 eleq1w 
 |-  ( a = d -> ( a e. L <-> d e. L ) )
18 17 notbid 
 |-  ( a = d -> ( -. a e. L <-> -. d e. L ) )
19 18 rspcev 
 |-  ( ( d e. P /\ -. d e. L ) -> E. a e. P -. a e. L )
20 19 ex 
 |-  ( d e. P -> ( -. d e. L -> E. a e. P -. a e. L ) )
21 12 16 20 3jaao 
 |-  ( ( b e. P /\ c e. P /\ d e. P ) -> ( ( -. b e. L \/ -. c e. L \/ -. d e. L ) -> E. a e. P -. a e. L ) )
22 3ianor 
 |-  ( -. ( b e. L /\ c e. L /\ d e. L ) <-> ( -. b e. L \/ -. c e. L \/ -. d e. L ) )
23 df-nel 
 |-  ( a e/ L <-> -. a e. L )
24 23 rexbii 
 |-  ( E. a e. P a e/ L <-> E. a e. P -. a e. L )
25 21 22 24 3imtr4g 
 |-  ( ( b e. P /\ c e. P /\ d e. P ) -> ( -. ( b e. L /\ c e. L /\ d e. L ) -> E. a e. P a e/ L ) )
26 8 25 syl9r 
 |-  ( ( b e. P /\ c e. P /\ d e. P ) -> ( A. l e. G -. ( b e. l /\ c e. l /\ d e. l ) -> ( L e. G -> E. a e. P a e/ L ) ) )
27 26 3expia 
 |-  ( ( b e. P /\ c e. P ) -> ( d e. P -> ( A. l e. G -. ( b e. l /\ c e. l /\ d e. l ) -> ( L e. G -> E. a e. P a e/ L ) ) ) )
28 27 rexlimdv 
 |-  ( ( b e. P /\ c e. P ) -> ( E. d e. P A. l e. G -. ( b e. l /\ c e. l /\ d e. l ) -> ( L e. G -> E. a e. P a e/ L ) ) )
29 28 rexlimivv 
 |-  ( E. b e. P E. c e. P E. d e. P A. l e. G -. ( b e. l /\ c e. l /\ d e. l ) -> ( L e. G -> E. a e. P a e/ L ) )
30 2 29 syl 
 |-  ( G e. Plig -> ( L e. G -> E. a e. P a e/ L ) )
31 30 imp 
 |-  ( ( G e. Plig /\ L e. G ) -> E. a e. P a e/ L )