Description: The Moore closure of a set is a subset of the base. Deduction form of mrcssv . (Contributed by David Moews, 1-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mrcssd.1 | |- ( ph -> A e. ( Moore ` X ) ) |
|
mrcssd.2 | |- N = ( mrCls ` A ) |
||
Assertion | mrcssvd | |- ( ph -> ( N ` B ) C_ X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mrcssd.1 | |- ( ph -> A e. ( Moore ` X ) ) |
|
2 | mrcssd.2 | |- N = ( mrCls ` A ) |
|
3 | 2 | mrcssv | |- ( A e. ( Moore ` X ) -> ( N ` B ) C_ X ) |
4 | 1 3 | syl | |- ( ph -> ( N ` B ) C_ X ) |