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

Metamath Proof Explorer

Theorem acsmre

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

Ref Expression
Assertion acsmre ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X

Proof

Step Hyp Ref Expression
1 isacs ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ⋃ f 𝒫 s ∩ Fin ⊆ s
2 1 simplbi ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X