Description: The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mrcfval.f | |
|
Assertion | mrcssv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mrcfval.f | |
|
2 | fvssunirn | |
|
3 | 1 | mrcf | |
4 | frn | |
|
5 | uniss | |
|
6 | 3 4 5 | 3syl | |
7 | mreuni | |
|
8 | 6 7 | sseqtrd | |
9 | 2 8 | sstrid | |