# Metamath Proof Explorer

## Theorem nsnlplig

Description: There is no "one-point line" in a planar incidence geometry. (Contributed by BJ, 2-Dec-2021) (Proof shortened by AV, 5-Dec-2021)

Ref Expression
Assertion nsnlplig ${⊢}{G}\in \mathrm{Plig}\to ¬\left\{{A}\right\}\in {G}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\bigcup {G}=\bigcup {G}$
2 1 l2p ${⊢}\left({G}\in \mathrm{Plig}\wedge \left\{{A}\right\}\in {G}\right)\to \exists {a}\in \bigcup {G}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {G}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in \left\{{A}\right\}\wedge {b}\in \left\{{A}\right\}\right)$
3 elsni ${⊢}{a}\in \left\{{A}\right\}\to {a}={A}$
4 elsni ${⊢}{b}\in \left\{{A}\right\}\to {b}={A}$
5 eqtr3 ${⊢}\left({a}={A}\wedge {b}={A}\right)\to {a}={b}$
6 eqneqall ${⊢}{a}={b}\to \left({a}\ne {b}\to ¬\left\{{A}\right\}\in {G}\right)$
7 5 6 syl ${⊢}\left({a}={A}\wedge {b}={A}\right)\to \left({a}\ne {b}\to ¬\left\{{A}\right\}\in {G}\right)$
8 3 4 7 syl2an ${⊢}\left({a}\in \left\{{A}\right\}\wedge {b}\in \left\{{A}\right\}\right)\to \left({a}\ne {b}\to ¬\left\{{A}\right\}\in {G}\right)$
9 8 impcom ${⊢}\left({a}\ne {b}\wedge \left({a}\in \left\{{A}\right\}\wedge {b}\in \left\{{A}\right\}\right)\right)\to ¬\left\{{A}\right\}\in {G}$
10 9 3impb ${⊢}\left({a}\ne {b}\wedge {a}\in \left\{{A}\right\}\wedge {b}\in \left\{{A}\right\}\right)\to ¬\left\{{A}\right\}\in {G}$
11 10 a1i ${⊢}\left({a}\in \bigcup {G}\wedge {b}\in \bigcup {G}\right)\to \left(\left({a}\ne {b}\wedge {a}\in \left\{{A}\right\}\wedge {b}\in \left\{{A}\right\}\right)\to ¬\left\{{A}\right\}\in {G}\right)$
12 11 rexlimivv ${⊢}\exists {a}\in \bigcup {G}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {G}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in \left\{{A}\right\}\wedge {b}\in \left\{{A}\right\}\right)\to ¬\left\{{A}\right\}\in {G}$
13 2 12 syl ${⊢}\left({G}\in \mathrm{Plig}\wedge \left\{{A}\right\}\in {G}\right)\to ¬\left\{{A}\right\}\in {G}$
14 13 pm2.01da ${⊢}{G}\in \mathrm{Plig}\to ¬\left\{{A}\right\}\in {G}$