Theorem mrcssv

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	|- F = ( mrCls ` C )
Assertion	mrcssv	|- ( C e. ( Moore ` X ) -> ( F ` U ) C_ X )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2		fvssunirn	|- ( F ` U ) C_ U. ran F
3	1	mrcf	|- ( C e. ( Moore ` X ) -> F : ~P X --> C )
4		frn	|- ( F : ~P X --> C -> ran F C_ C )
5		uniss	|- ( ran F C_ C -> U. ran F C_ U. C )
6	3 4 5	3syl	|- ( C e. ( Moore ` X ) -> U. ran F C_ U. C )
7		mreuni	|- ( C e. ( Moore ` X ) -> U. C = X )
8	6 7	sseqtrd	|- ( C e. ( Moore ` X ) -> U. ran F C_ X )
9	2 8	sstrid	|- ( C e. ( Moore ` X ) -> ( F ` U ) C_ X )