# Metamath Proof Explorer

## Theorem ispligb

Description: The predicate "is a planar incidence geometry". (Contributed by BJ, 2-Dec-2021)

Ref Expression
Hypothesis isplig.1 ${⊢}{P}=\bigcup {G}$
Assertion ispligb ${⊢}{G}\in \mathrm{Plig}↔\left({G}\in \mathrm{V}\wedge \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)$

### Proof

Step Hyp Ref Expression
1 isplig.1 ${⊢}{P}=\bigcup {G}$
2 elex ${⊢}{G}\in \mathrm{Plig}\to {G}\in \mathrm{V}$
3 1 isplig ${⊢}{G}\in \mathrm{V}\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)$
4 2 3 biadanii ${⊢}{G}\in \mathrm{Plig}↔\left({G}\in \mathrm{V}\wedge \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)$