Metamath Proof Explorer

Theorem isacs3

Description: A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isacs3 ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C

Proof

Step Hyp Ref Expression
1 isacs3lem ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
2 eqid ⊢ mrCls ⁡ C = mrCls ⁡ C
3 2 isacs4lem ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → C ∈ Moore ⁡ X ∧ ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → mrCls ⁡ C ⁡ ⋃ t = ⋃ mrCls ⁡ C t
4 2 isacs4 ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → mrCls ⁡ C ⁡ ⋃ t = ⋃ mrCls ⁡ C t
5 3 4 sylibr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → C ∈ ACS ⁡ X
6 1 5 impbii ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C