# Metamath Proof Explorer

## Theorem l2p

Description: For any line in a planar incidence geometry, there exist two different points on the line. (Contributed by AV, 28-Nov-2021)

Ref Expression
Hypothesis l2p.1 ${⊢}{P}=\bigcup {G}$
Assertion l2p ${⊢}\left({G}\in \mathrm{Plig}\wedge {L}\in {G}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {L}\wedge {b}\in {L}\right)$

### Proof

Step Hyp Ref Expression
1 l2p.1 ${⊢}{P}=\bigcup {G}$
2 1 isplig ${⊢}{G}\in \mathrm{Plig}\to \left({G}\in \mathrm{Plig}↔\left(\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {G}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)\right)$
3 eleq2 ${⊢}{l}={L}\to \left({a}\in {l}↔{a}\in {L}\right)$
4 eleq2 ${⊢}{l}={L}\to \left({b}\in {l}↔{b}\in {L}\right)$
5 3 4 3anbi23d ${⊢}{l}={L}\to \left(\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)↔\left({a}\ne {b}\wedge {a}\in {L}\wedge {b}\in {L}\right)\right)$
6 5 2rexbidv ${⊢}{l}={L}\to \left(\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)↔\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {L}\wedge {b}\in {L}\right)\right)$
7 6 rspccv ${⊢}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {L}\wedge {b}\in {L}\right)\right)$
8 7 3ad2ant2 ${⊢}\left(\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {G}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {L}\wedge {b}\in {L}\right)\right)$
9 2 8 syl6bi ${⊢}{G}\in \mathrm{Plig}\to \left({G}\in \mathrm{Plig}\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {L}\wedge {b}\in {L}\right)\right)\right)$
10 9 pm2.43i ${⊢}{G}\in \mathrm{Plig}\to \left({L}\in {G}\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {L}\wedge {b}\in {L}\right)\right)$
11 10 imp ${⊢}\left({G}\in \mathrm{Plig}\wedge {L}\in {G}\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {L}\wedge {b}\in {L}\right)$