Theorem mrcss

Description: Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2		sstr2	|- ( U C_ V -> ( V C_ s -> U C_ s ) )
3	2	adantr	|- ( ( U C_ V /\ s e. C ) -> ( V C_ s -> U C_ s ) )
4	3	ss2rabdv	|- ( U C_ V -> { s e. C | V C_ s } C_ { s e. C | U C_ s } )
5		intss	|- ( { s e. C | V C_ s } C_ { s e. C | U C_ s } -> |^| { s e. C | U C_ s } C_ |^| { s e. C | V C_ s } )
6	4 5	syl	|- ( U C_ V -> |^| { s e. C | U C_ s } C_ |^| { s e. C | V C_ s } )
7	6	3ad2ant2	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> |^| { s e. C | U C_ s } C_ |^| { s e. C | V C_ s } )
8		simp1	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> C e. ( Moore ` X ) )
9		sstr	|- ( ( U C_ V /\ V C_ X ) -> U C_ X )
10	9	3adant1	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> U C_ X )
11	1	mrcval	|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) = |^| { s e. C | U C_ s } )
12	8 10 11	syl2anc	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> ( F ` U ) = |^| { s e. C | U C_ s } )
13	1	mrcval	|- ( ( C e. ( Moore ` X ) /\ V C_ X ) -> ( F ` V ) = |^| { s e. C | V C_ s } )
14	13	3adant2	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> ( F ` V ) = |^| { s e. C | V C_ s } )
15	7 12 14	3sstr4d	|- ( ( C e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> ( F ` U ) C_ ( F ` V ) )