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	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 ⊆ 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ismre	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) )
2	1	simp1bi	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 ⊆ 𝒫 𝑋 )