# 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}=\bigcup {G}$
Assertion lpni ${⊢}\left({G}\in \mathrm{Plig}\wedge {L}\in {G}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}$

### Proof

Step Hyp Ref Expression
1 l2p.1 ${⊢}{P}=\bigcup {G}$
2 1 tncp ${⊢}{G}\in \mathrm{Plig}\to \exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({b}\in {l}\wedge {c}\in {l}\wedge {d}\in {l}\right)$
3 eleq2 ${⊢}{l}={L}\to \left({b}\in {l}↔{b}\in {L}\right)$
4 eleq2 ${⊢}{l}={L}\to \left({c}\in {l}↔{c}\in {L}\right)$
5 eleq2 ${⊢}{l}={L}\to \left({d}\in {l}↔{d}\in {L}\right)$
6 3 4 5 3anbi123d ${⊢}{l}={L}\to \left(\left({b}\in {l}\wedge {c}\in {l}\wedge {d}\in {l}\right)↔\left({b}\in {L}\wedge {c}\in {L}\wedge {d}\in {L}\right)\right)$
7 6 notbid ${⊢}{l}={L}\to \left(¬\left({b}\in {l}\wedge {c}\in {l}\wedge {d}\in {l}\right)↔¬\left({b}\in {L}\wedge {c}\in {L}\wedge {d}\in {L}\right)\right)$
8 7 rspccv ${⊢}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({b}\in {l}\wedge {c}\in {l}\wedge {d}\in {l}\right)\to \left({L}\in {G}\to ¬\left({b}\in {L}\wedge {c}\in {L}\wedge {d}\in {L}\right)\right)$
9 eleq1w ${⊢}{a}={b}\to \left({a}\in {L}↔{b}\in {L}\right)$
10 9 notbid ${⊢}{a}={b}\to \left(¬{a}\in {L}↔¬{b}\in {L}\right)$
11 10 rspcev ${⊢}\left({b}\in {P}\wedge ¬{b}\in {L}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}¬{a}\in {L}$
12 11 ex ${⊢}{b}\in {P}\to \left(¬{b}\in {L}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}¬{a}\in {L}\right)$
13 eleq1w ${⊢}{a}={c}\to \left({a}\in {L}↔{c}\in {L}\right)$
14 13 notbid ${⊢}{a}={c}\to \left(¬{a}\in {L}↔¬{c}\in {L}\right)$
15 14 rspcev ${⊢}\left({c}\in {P}\wedge ¬{c}\in {L}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}¬{a}\in {L}$
16 15 ex ${⊢}{c}\in {P}\to \left(¬{c}\in {L}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}¬{a}\in {L}\right)$
17 eleq1w ${⊢}{a}={d}\to \left({a}\in {L}↔{d}\in {L}\right)$
18 17 notbid ${⊢}{a}={d}\to \left(¬{a}\in {L}↔¬{d}\in {L}\right)$
19 18 rspcev ${⊢}\left({d}\in {P}\wedge ¬{d}\in {L}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}¬{a}\in {L}$
20 19 ex ${⊢}{d}\in {P}\to \left(¬{d}\in {L}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}¬{a}\in {L}\right)$
21 12 16 20 3jaao ${⊢}\left({b}\in {P}\wedge {c}\in {P}\wedge {d}\in {P}\right)\to \left(\left(¬{b}\in {L}\vee ¬{c}\in {L}\vee ¬{d}\in {L}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}¬{a}\in {L}\right)$
22 3ianor ${⊢}¬\left({b}\in {L}\wedge {c}\in {L}\wedge {d}\in {L}\right)↔\left(¬{b}\in {L}\vee ¬{c}\in {L}\vee ¬{d}\in {L}\right)$
23 df-nel ${⊢}{a}\notin {L}↔¬{a}\in {L}$
24 23 rexbii ${⊢}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}↔\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}¬{a}\in {L}$
25 21 22 24 3imtr4g ${⊢}\left({b}\in {P}\wedge {c}\in {P}\wedge {d}\in {P}\right)\to \left(¬\left({b}\in {L}\wedge {c}\in {L}\wedge {d}\in {L}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}\right)$
26 8 25 syl9r ${⊢}\left({b}\in {P}\wedge {c}\in {P}\wedge {d}\in {P}\right)\to \left(\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({b}\in {l}\wedge {c}\in {l}\wedge {d}\in {l}\right)\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}\right)\right)$
27 26 3expia ${⊢}\left({b}\in {P}\wedge {c}\in {P}\right)\to \left({d}\in {P}\to \left(\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({b}\in {l}\wedge {c}\in {l}\wedge {d}\in {l}\right)\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}\right)\right)\right)$
28 27 rexlimdv ${⊢}\left({b}\in {P}\wedge {c}\in {P}\right)\to \left(\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({b}\in {l}\wedge {c}\in {l}\wedge {d}\in {l}\right)\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}\right)\right)$
29 28 rexlimivv ${⊢}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({b}\in {l}\wedge {c}\in {l}\wedge {d}\in {l}\right)\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}\right)$
30 2 29 syl ${⊢}{G}\in \mathrm{Plig}\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}\right)$
31 30 imp ${⊢}\left({G}\in \mathrm{Plig}\wedge {L}\in {G}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}{a}\notin {L}$