Theorem ispligb

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

	Ref	Expression
Hypothesis	isplig.1	⊢ 𝑃 = ∪ 𝐺
Assertion	ispligb	⊢ ( 𝐺 ∈ Plig ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isplig.1	⊢ 𝑃 = ∪ 𝐺
2		elex	⊢ ( 𝐺 ∈ Plig → 𝐺 ∈ V )
3	1	isplig	⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ Plig ↔ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )
4	2 3	biadanii	⊢ ( 𝐺 ∈ Plig ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )