This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → ∪ 𝑠 ∈ 𝐶 ) ) )