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=⋃G
Assertion ispligb ⊢G∈Plig↔G∈V∧∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l∧∀l∈G∃a∈P∃b∈Pa≠b∧a∈l∧b∈l∧∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l

Proof

Step Hyp Ref Expression
1 isplig.1 ⊢P=⋃G
2 elex ⊢G∈Plig→G∈V
3 1 isplig ⊢G∈V→G∈Plig↔∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l∧∀l∈G∃a∈P∃b∈Pa≠b∧a∈l∧b∈l∧∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l
4 2 3 biadanii ⊢G∈Plig↔G∈V∧∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l∧∀l∈G∃a∈P∃b∈Pa≠b∧a∈l∧b∈l∧∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l