Metamath Proof Explorer

Theorem ss2mcls

Description: The closure is monotonic under subsets of the original set of expressions and the set of disjoint variable conditions. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclsval.d 
|- D = ( mDV ` T )
mclsval.e 
|- E = ( mEx ` T )
mclsval.c 
|- C = ( mCls ` T )
mclsval.1 
|- ( ph -> T e. mFS )
mclsval.2 
|- ( ph -> K C_ D )
mclsval.3 
|- ( ph -> B C_ E )
ss2mcls.4 
|- ( ph -> X C_ K )
ss2mcls.5 
|- ( ph -> Y C_ B )
Assertion ss2mcls 
|- ( ph -> ( X C Y ) C_ ( K C B ) )

Proof

Step Hyp Ref Expression
1 mclsval.d 
 |-  D = ( mDV ` T )
2 mclsval.e 
 |-  E = ( mEx ` T )
3 mclsval.c 
 |-  C = ( mCls ` T )
4 mclsval.1 
 |-  ( ph -> T e. mFS )
5 mclsval.2 
 |-  ( ph -> K C_ D )
6 mclsval.3 
 |-  ( ph -> B C_ E )
7 ss2mcls.4 
 |-  ( ph -> X C_ K )
8 ss2mcls.5 
 |-  ( ph -> Y C_ B )
9 unss1 
 |-  ( Y C_ B -> ( Y u. ran ( mVH ` T ) ) C_ ( B u. ran ( mVH ` T ) ) )
10 sstr2 
 |-  ( ( Y u. ran ( mVH ` T ) ) C_ ( B u. ran ( mVH ` T ) ) -> ( ( B u. ran ( mVH ` T ) ) C_ c -> ( Y u. ran ( mVH ` T ) ) C_ c ) )
11 8 9 10 3syl 
 |-  ( ph -> ( ( B u. ran ( mVH ` T ) ) C_ c -> ( Y u. ran ( mVH ` T ) ) C_ c ) )
12 sstr2 
 |-  ( ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X -> ( X C_ K -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) )
13 7 12 syl5com 
 |-  ( ph -> ( ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) )
14 13 imim2d 
 |-  ( ph -> ( ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) -> ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) )
15 14 2alimdv 
 |-  ( ph -> ( A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) -> A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) )
16 15 anim2d 
 |-  ( ph -> ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) ) )
17 16 imim1d 
 |-  ( ph -> ( ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) -> ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) )
18 17 ralimdv 
 |-  ( ph -> ( A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) )
19 18 imim2d 
 |-  ( ph -> ( ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) -> ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) )
20 19 alimdv 
 |-  ( ph -> ( A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) -> A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) )
21 20 2alimdv 
 |-  ( ph -> ( A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) -> A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) )
22 11 21 anim12d 
 |-  ( ph -> ( ( ( B u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) -> ( ( Y u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) ) )
23 22 ss2abdv 
 |-  ( ph -> { c | ( ( B u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ { c | ( ( Y u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) } )
24 intss 
 |-  ( { c | ( ( B u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ { c | ( ( Y u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) } -> |^| { c | ( ( Y u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) } C_ |^| { c | ( ( B u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
25 23 24 syl 
 |-  ( ph -> |^| { c | ( ( Y u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) } C_ |^| { c | ( ( B u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
26 7 5 sstrd 
 |-  ( ph -> X C_ D )
27 8 6 sstrd 
 |-  ( ph -> Y C_ E )
28 eqid 
 |-  ( mVH ` T ) = ( mVH ` T )
29 eqid 
 |-  ( mAx ` T ) = ( mAx ` T )
30 eqid 
 |-  ( mSubst ` T ) = ( mSubst ` T )
31 eqid 
 |-  ( mVars ` T ) = ( mVars ` T )
32 1 2 3 4 26 27 28 29 30 31 mclsval 
 |-  ( ph -> ( X C Y ) = |^| { c | ( ( Y u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ X ) ) -> ( s ` p ) e. c ) ) ) } )
33 1 2 3 4 5 6 28 29 30 31 mclsval 
 |-  ( ph -> ( K C B ) = |^| { c | ( ( B u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
34 25 32 33 3sstr4d 
 |-  ( ph -> ( X C Y ) C_ ( K C B ) )