Theorem mrcsscl

Description: The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2		mress	|- ( ( C e. ( Moore ` X ) /\ V e. C ) -> V C_ X )
3	2	3adant2	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> V C_ X )
4	1	mrcss	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> ( F ` U ) C_ ( F ` V ) )
5	3 4	syld3an3	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> ( F ` U ) C_ ( F ` V ) )
6	1	mrcid	|- ( ( C e. ( Moore ` X ) /\ V e. C ) -> ( F ` V ) = V )
7	6	3adant2	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> ( F ` V ) = V )
8	5 7	sseqtrd	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> ( F ` U ) C_ V )