Metamath Proof Explorer

Theorem acsfiel

Description: A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis isacs2.f ⊢ F = mrCls ⁡ C
Assertion acsfiel ⊢ C ∈ ACS ⁡ X → S ∈ C ↔ S ⊆ X ∧ ∀ y ∈ 𝒫 S ∩ Fin F ⁡ y ⊆ S

Proof

Step Hyp Ref Expression
1 isacs2.f ⊢ F = mrCls ⁡ C
2 acsmre ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X
3 mress ⊢ C ∈ Moore ⁡ X ∧ S ∈ C → S ⊆ X
4 2 3 sylan ⊢ C ∈ ACS ⁡ X ∧ S ∈ C → S ⊆ X
5 4 ex ⊢ C ∈ ACS ⁡ X → S ∈ C → S ⊆ X
6 5 pm4.71rd ⊢ C ∈ ACS ⁡ X → S ∈ C ↔ S ⊆ X ∧ S ∈ C
7 eleq1 ⊢ s = S → s ∈ C ↔ S ∈ C
8 pweq ⊢ s = S → 𝒫 s = 𝒫 S
9 8 ineq1d ⊢ s = S → 𝒫 s ∩ Fin = 𝒫 S ∩ Fin
10 sseq2 ⊢ s = S → F ⁡ y ⊆ s ↔ F ⁡ y ⊆ S
11 9 10 raleqbidv ⊢ s = S → ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s ↔ ∀ y ∈ 𝒫 S ∩ Fin F ⁡ y ⊆ S
12 7 11 bibi12d ⊢ s = S → s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s ↔ S ∈ C ↔ ∀ y ∈ 𝒫 S ∩ Fin F ⁡ y ⊆ S
13 1 isacs2 ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
14 13 simprbi ⊢ C ∈ ACS ⁡ X → ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
15 14 adantr ⊢ C ∈ ACS ⁡ X ∧ S ⊆ X → ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
16 elfvdm ⊢ C ∈ ACS ⁡ X → X ∈ dom ⁡ ACS
17 elpw2g ⊢ X ∈ dom ⁡ ACS → S ∈ 𝒫 X ↔ S ⊆ X
18 16 17 syl ⊢ C ∈ ACS ⁡ X → S ∈ 𝒫 X ↔ S ⊆ X
19 18 biimpar ⊢ C ∈ ACS ⁡ X ∧ S ⊆ X → S ∈ 𝒫 X
20 12 15 19 rspcdva ⊢ C ∈ ACS ⁡ X ∧ S ⊆ X → S ∈ C ↔ ∀ y ∈ 𝒫 S ∩ Fin F ⁡ y ⊆ S
21 20 pm5.32da ⊢ C ∈ ACS ⁡ X → S ⊆ X ∧ S ∈ C ↔ S ⊆ X ∧ ∀ y ∈ 𝒫 S ∩ Fin F ⁡ y ⊆ S
22 6 21 bitrd ⊢ C ∈ ACS ⁡ X → S ∈ C ↔ S ⊆ X ∧ ∀ y ∈ 𝒫 S ∩ Fin F ⁡ y ⊆ S