Metamath Proof Explorer

Theorem ssmclslem

Description: Lemma for ssmcls . (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 )
ssmclslem.h 
|- H = ( mVH ` T )
Assertion ssmclslem 
|- ( ph -> ( B u. ran H ) 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 ssmclslem.h 
 |-  H = ( mVH ` T )
8 simpl 
 |-  ( ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( H ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) -> ( B u. ran H ) C_ c )
9 8 a1i 
 |-  ( ph -> ( ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( H ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) -> ( B u. ran H ) C_ c ) )
10 9 alrimiv 
 |-  ( ph -> A. c ( ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( H ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) -> ( B u. ran H ) C_ c ) )
11 ssintab 
 |-  ( ( B u. ran H ) C_ |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( H ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } <-> A. c ( ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( H ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) -> ( B u. ran H ) C_ c ) )
12 10 11 sylibr 
 |-  ( ph -> ( B u. ran H ) C_ |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( H ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
13 eqid 
 |-  ( mAx ` T ) = ( mAx ` T )
14 eqid 
 |-  ( mSubst ` T ) = ( mSubst ` T )
15 eqid 
 |-  ( mVars ` T ) = ( mVars ` T )
16 1 2 3 4 5 6 7 13 14 15 mclsval 
 |-  ( ph -> ( K C B ) = |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( H ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
17 12 16 sseqtrrd 
 |-  ( ph -> ( B u. ran H ) C_ ( K C B ) )