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∈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 unieq ⊢x=G→⋃x=⋃G
3 2 1 eqtr4di ⊢x=G→⋃x=P
4 reueq1 ⊢x=G→∃!l∈xa∈l∧b∈l↔∃!l∈Ga∈l∧b∈l
5 4 imbi2d ⊢x=G→a≠b→∃!l∈xa∈l∧b∈l↔a≠b→∃!l∈Ga∈l∧b∈l
6 3 5 raleqbidv ⊢x=G→∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l↔∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l
7 3 6 raleqbidv ⊢x=G→∀a∈⋃x∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l↔∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l
8 3 rexeqdv ⊢x=G→∃b∈⋃xa≠b∧a∈l∧b∈l↔∃b∈Pa≠b∧a∈l∧b∈l
9 3 8 rexeqbidv ⊢x=G→∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l↔∃a∈P∃b∈Pa≠b∧a∈l∧b∈l
10 9 raleqbi1dv ⊢x=G→∀l∈x∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l↔∀l∈G∃a∈P∃b∈Pa≠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∈⋃xa≠b→∃!l∈xa∈l∧b∈l∧∀l∈x∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l∧∃a∈⋃x∃b∈⋃x∃c∈⋃x∀l∈x¬a∈l∧b∈l∧c∈l↔∀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
16 df-plig ⊢Plig=x|∀a∈⋃x∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l∧∀l∈x∃a∈⋃x∃b∈⋃xa≠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∈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