Metamath Proof Explorer

Theorem isacs4

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

Ref Expression
Hypothesis acsdrscl.f ⊢F=mrCls⁡C
Assertion isacs4 ⊢C∈ACS⁡X↔C∈Moore⁡X∧∀s∈𝒫𝒫XtoInc⁡s∈Dirset→F⁡⋃s=⋃Fs

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢F=mrCls⁡C
2 isacs3lem ⊢C∈ACS⁡X→C∈Moore⁡X∧∀t∈𝒫CtoInc⁡t∈Dirset→⋃t∈C
3 1 isacs4lem ⊢C∈Moore⁡X∧∀t∈𝒫CtoInc⁡t∈Dirset→⋃t∈C→C∈Moore⁡X∧∀s∈𝒫𝒫XtoInc⁡s∈Dirset→F⁡⋃s=⋃Fs
4 2 3 syl ⊢C∈ACS⁡X→C∈Moore⁡X∧∀s∈𝒫𝒫XtoInc⁡s∈Dirset→F⁡⋃s=⋃Fs
5 1 isacs5lem ⊢C∈Moore⁡X∧∀s∈𝒫𝒫XtoInc⁡s∈Dirset→F⁡⋃s=⋃Fs→C∈Moore⁡X∧∀t∈𝒫XF⁡t=⋃F𝒫t∩Fin
6 1 isacs5 ⊢C∈ACS⁡X↔C∈Moore⁡X∧∀t∈𝒫XF⁡t=⋃F𝒫t∩Fin
7 5 6 sylibr ⊢C∈Moore⁡X∧∀s∈𝒫𝒫XtoInc⁡s∈Dirset→F⁡⋃s=⋃Fs→C∈ACS⁡X
8 4 7 impbii ⊢C∈ACS⁡X↔C∈Moore⁡X∧∀s∈𝒫𝒫XtoInc⁡s∈Dirset→F⁡⋃s=⋃Fs