Metamath Proof Explorer


Theorem mre1cl

Description: In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mre1cl ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋𝐶 )

Proof

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