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∈𝒫CtoInc⁡s∈Dirset→⋃s∈C

Proof

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