# Metamath Proof Explorer

## Theorem isplig

Description: The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009)

Ref Expression
Hypothesis isplig.1 ${⊢}{P}=\bigcup {G}$
Assertion isplig ${⊢}{G}\in {A}\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)$

### Proof

Step Hyp Ref Expression
1 isplig.1 ${⊢}{P}=\bigcup {G}$
2 unieq ${⊢}{x}={G}\to \bigcup {x}=\bigcup {G}$
3 2 1 eqtr4di ${⊢}{x}={G}\to \bigcup {x}={P}$
4 reueq1 ${⊢}{x}={G}\to \left(\exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)↔\exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)$
5 4 imbi2d ${⊢}{x}={G}\to \left(\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)↔\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\right)$
6 3 5 raleqbidv ${⊢}{x}={G}\to \left(\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)↔\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)\right)$
7 3 6 raleqbidv ${⊢}{x}={G}\to \left(\forall {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)↔\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)\right)$
8 3 rexeqdv ${⊢}{x}={G}\to \left(\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)↔\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\right)$
9 3 8 rexeqbidv ${⊢}{x}={G}\to \left(\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\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)$
10 9 raleqbi1dv ${⊢}{x}={G}\to \left(\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)↔\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)\right)$
11 raleq ${⊢}{x}={G}\to \left(\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)↔\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)$
12 3 11 rexeqbidv ${⊢}{x}={G}\to \left(\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)↔\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)$
13 3 12 rexeqbidv ${⊢}{x}={G}\to \left(\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)↔\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)$
14 3 13 rexeqbidv ${⊢}{x}={G}\to \left(\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)↔\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)$
15 7 10 14 3anbi123d ${⊢}{x}={G}\to \left(\left(\forall {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {x}\phantom{\rule{.4em}{0ex}}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)↔\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)$
16 df-plig ${⊢}\mathrm{Plig}=\left\{{x}|\left(\forall {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {x}\phantom{\rule{.4em}{0ex}}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)\right\}$
17 15 16 elab2g ${⊢}{G}\in {A}\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)$