Theorem acsmre

Description: Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015)

	Ref	Expression
Assertion	acsmre	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		isacs	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ) ) ) )
2	1	simplbi	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )