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 = ⋃ G
Assertion isplig ⊢ G ∈ A → 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

Proof

Step Hyp Ref Expression
1 isplig.1 ⊢ P = ⋃ G
2 unieq ⊢ x = G → ⋃ x = ⋃ G
3 2 1 eqtr4di ⊢ x = G → ⋃ x = P
4 reueq1 ⊢ x = G → ∃! l ∈ x a ∈ l ∧ b ∈ l ↔ ∃! l ∈ G a ∈ l ∧ b ∈ l
5 4 imbi2d ⊢ x = G → a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ↔ a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l
6 3 5 raleqbidv ⊢ x = G → ∀ b ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ↔ ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l
7 3 6 raleqbidv ⊢ x = G → ∀ a ∈ ⋃ x ∀ b ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ↔ ∀ a ∈ P ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l
8 3 rexeqdv ⊢ x = G → ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l ↔ ∃ b ∈ P a ≠ b ∧ a ∈ l ∧ b ∈ l
9 3 8 rexeqbidv ⊢ x = G → ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l ↔ ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ l ∧ b ∈ l
10 9 raleqbi1dv ⊢ x = G → ∀ l ∈ x ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l ↔ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ l ∧ b ∈ l
11 raleq ⊢ x = G → ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l ↔ ∀ l ∈ G ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l
12 3 11 rexeqbidv ⊢ x = G → ∃ c ∈ ⋃ x ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l ↔ ∃ c ∈ P ∀ l ∈ G ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l
13 3 12 rexeqbidv ⊢ x = G → ∃ b ∈ ⋃ x ∃ c ∈ ⋃ x ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l ↔ ∃ b ∈ P ∃ c ∈ P ∀ l ∈ G ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l
14 3 13 rexeqbidv ⊢ x = G → ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x ∃ c ∈ ⋃ x ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l ↔ ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ∀ l ∈ G ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l
15 7 10 14 3anbi123d ⊢ x = G → ∀ a ∈ ⋃ x ∀ b ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ∧ ∀ l ∈ x ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l ∧ ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x ∃ c ∈ ⋃ x ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l ↔ ∀ 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
16 df-plig ⊢ Plig = x | ∀ a ∈ ⋃ x ∀ b ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ∧ ∀ l ∈ x ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l ∧ ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x ∃ c ∈ ⋃ x ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l
17 15 16 elab2g ⊢ G ∈ A → 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