Description: In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | mre1cl | ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismre | ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) ) | |
2 | 1 | simp2bi | ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 ) |