Metamath Proof Explorer

Theorem isacs

Description: A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isacs ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s

Proof

Step Hyp Ref Expression
1 elfvex ⊢ C ∈ ACS ⁡ X → X ∈ V
2 elfvex ⊢ C ∈ Moore ⁡ X → X ∈ V
3 2 adantr ⊢ C ∈ Moore ⁡ X ∧ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s → X ∈ V
4 fveq2 ⊢ x = X → Moore ⁡ x = Moore ⁡ X
5 pweq ⊢ x = X → 𝒫 x = 𝒫 X
6 5 5 feq23d ⊢ x = X → f : 𝒫 x ⟶ 𝒫 x ↔ f : 𝒫 X ⟶ 𝒫 X
7 5 raleqdv ⊢ x = X → ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ↔ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
8 6 7 anbi12d ⊢ x = X → f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ↔ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
9 8 exbidv ⊢ x = X → ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ↔ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
10 4 9 rabeqbidv ⊢ x = X → c ∈ Moore ⁡ x | ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s = c ∈ Moore ⁡ X | ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
11 df-acs ⊢ ACS = x ∈ V ⟼ c ∈ Moore ⁡ x | ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ s ∈ 𝒫 x s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
12 fvex ⊢ Moore ⁡ X ∈ V
13 12 rabex ⊢ c ∈ Moore ⁡ X | ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ∈ V
14 10 11 13 fvmpt ⊢ X ∈ V → ACS ⁡ X = c ∈ Moore ⁡ X | ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
15 14 eleq2d ⊢ X ∈ V → C ∈ ACS ⁡ X ↔ C ∈ c ∈ Moore ⁡ X | ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
16 eleq2 ⊢ c = C → s ∈ c ↔ s ∈ C
17 16 bibi1d ⊢ c = C → s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ↔ s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
18 17 ralbidv ⊢ c = C → ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ↔ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
19 18 anbi2d ⊢ c = C → f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ↔ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
20 19 exbidv ⊢ c = C → ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ↔ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
21 20 elrab ⊢ C ∈ c ∈ Moore ⁡ X | ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ c ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s ↔ C ∈ Moore ⁡ X ∧ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
22 15 21 bitrdi ⊢ X ∈ V → C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
23 1 3 22 pm5.21nii ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s