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 e. ( Moore ` X ) -> C C_ ~P X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ismre | |- ( C e. ( Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) |
|
| 2 | 1 | simp1bi | |- ( C e. ( Moore ` X ) -> C C_ ~P X ) |