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 ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 isacs3lem ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) )
2 eqid ( mrCls ‘ 𝐶 ) = ( mrCls ‘ 𝐶 )
3 2 isacs4lem ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( ( mrCls ‘ 𝐶 ) ‘ 𝑡 ) = ( ( mrCls ‘ 𝐶 ) “ 𝑡 ) ) ) )
4 2 isacs4 ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( ( mrCls ‘ 𝐶 ) ‘ 𝑡 ) = ( ( mrCls ‘ 𝐶 ) “ 𝑡 ) ) ) )
5 3 4 sylibr ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) )
6 1 5 impbii ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) )