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 ∈ 𝒫 𝒫 X toInc ⁡ s ∈ Dirset → F ⁡ ⋃ s = ⋃ F s

Proof

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