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