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	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	isacs4	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		acsdrscl.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2		isacs3lem	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ∪ 𝑡 ∈ 𝐶 ) ) )
3	1	isacs4lem	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ∪ 𝑡 ∈ 𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) )
4	2 3	syl	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) )
5	1	isacs5lem	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑡 ) = ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ) )
6	1	isacs5	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑡 ) = ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ) )
7	5 6	sylibr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) )
8	4 7	impbii	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) )