Theorem mrcssid

Description: The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrcfval.f	|- F = ( mrCls ` C )
Assertion	mrcssid	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> U C_ ( F ` U ) )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2		ssintub	|- U C_ |^| { s e. C | U C_ s }
3	1	mrcval	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) = |^| { s e. C | U C_ s } )
4	2 3	sseqtrrid	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> U C_ ( F ` U ) )