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

Metamath Proof Explorer

Theorem mresspw

Description: A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mresspw ⊢ C ∈ Moore ⁡ X → C ⊆ 𝒫 X

Proof

Step Hyp Ref Expression
1 ismre ⊢ C ∈ Moore ⁡ X ↔ C ⊆ 𝒫 X ∧ X ∈ C ∧ ∀ s ∈ 𝒫 C s ≠ ∅ → ⋂ s ∈ C
2 1 simp1bi ⊢ C ∈ Moore ⁡ X → C ⊆ 𝒫 X