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 ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ∧ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ 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 ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ∧ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ 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 ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ∧ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ l ∧ b ∈ l ∧ ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ∀ l ∈ G ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l