This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )