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=⋃G
Assertion lpni ⊢G∈Plig∧L∈G→∃a∈Pa∉L

Proof

Step Hyp Ref Expression
1 l2p.1 ⊢P=⋃G
2 1 tncp ⊢G∈Plig→∃b∈P∃c∈P∃d∈P∀l∈G¬b∈l∧c∈l∧d∈l
3 eleq2 ⊢l=L→b∈l↔b∈L
4 eleq2 ⊢l=L→c∈l↔c∈L
5 eleq2 ⊢l=L→d∈l↔d∈L
6 3 4 5 3anbi123d ⊢l=L→b∈l∧c∈l∧d∈l↔b∈L∧c∈L∧d∈L
7 6 notbid ⊢l=L→¬b∈l∧c∈l∧d∈l↔¬b∈L∧c∈L∧d∈L
8 7 rspccv ⊢∀l∈G¬b∈l∧c∈l∧d∈l→L∈G→¬b∈L∧c∈L∧d∈L
9 eleq1w ⊢a=b→a∈L↔b∈L
10 9 notbid ⊢a=b→¬a∈L↔¬b∈L
11 10 rspcev ⊢b∈P∧¬b∈L→∃a∈P¬a∈L
12 11 ex ⊢b∈P→¬b∈L→∃a∈P¬a∈L
13 eleq1w ⊢a=c→a∈L↔c∈L
14 13 notbid ⊢a=c→¬a∈L↔¬c∈L
15 14 rspcev ⊢c∈P∧¬c∈L→∃a∈P¬a∈L
16 15 ex ⊢c∈P→¬c∈L→∃a∈P¬a∈L
17 eleq1w ⊢a=d→a∈L↔d∈L
18 17 notbid ⊢a=d→¬a∈L↔¬d∈L
19 18 rspcev ⊢d∈P∧¬d∈L→∃a∈P¬a∈L
20 19 ex ⊢d∈P→¬d∈L→∃a∈P¬a∈L
21 12 16 20 3jaao ⊢b∈P∧c∈P∧d∈P→¬b∈L∨¬c∈L∨¬d∈L→∃a∈P¬a∈L
22 3ianor ⊢¬b∈L∧c∈L∧d∈L↔¬b∈L∨¬c∈L∨¬d∈L
23 df-nel ⊢a∉L↔¬a∈L
24 23 rexbii ⊢∃a∈Pa∉L↔∃a∈P¬a∈L
25 21 22 24 3imtr4g ⊢b∈P∧c∈P∧d∈P→¬b∈L∧c∈L∧d∈L→∃a∈Pa∉L
26 8 25 syl9r ⊢b∈P∧c∈P∧d∈P→∀l∈G¬b∈l∧c∈l∧d∈l→L∈G→∃a∈Pa∉L
27 26 3expia ⊢b∈P∧c∈P→d∈P→∀l∈G¬b∈l∧c∈l∧d∈l→L∈G→∃a∈Pa∉L
28 27 rexlimdv ⊢b∈P∧c∈P→∃d∈P∀l∈G¬b∈l∧c∈l∧d∈l→L∈G→∃a∈Pa∉L
29 28 rexlimivv ⊢∃b∈P∃c∈P∃d∈P∀l∈G¬b∈l∧c∈l∧d∈l→L∈G→∃a∈Pa∉L
30 2 29 syl ⊢G∈Plig→L∈G→∃a∈Pa∉L
31 30 imp ⊢G∈Plig∧L∈G→∃a∈Pa∉L