Metamath Proof Explorer

Theorem mclsssvlem

Description: Lemma for mclsssv . (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 )
mclsval.h 
|- H = ( mVH ` T )
mclsval.a 
|- A = ( mAx ` T )
mclsval.s 
|- S = ( mSubst ` T )
mclsval.v 
|- V = ( mVars ` T )
Assertion mclsssvlem 
|- ( ph -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ E )

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 mclsval.h 
 |-  H = ( mVH ` T )
8 mclsval.a 
 |-  A = ( mAx ` T )
9 mclsval.s 
 |-  S = ( mSubst ` T )
10 mclsval.v 
 |-  V = ( mVars ` T )
11 eqid 
 |-  ( mVR ` T ) = ( mVR ` T )
12 11 2 7 mvhf 
 |-  ( T e. mFS -> H : ( mVR ` T ) --> E )
13 4 12 syl 
 |-  ( ph -> H : ( mVR ` T ) --> E )
14 13 frnd 
 |-  ( ph -> ran H C_ E )
15 6 14 unssd 
 |-  ( ph -> ( B u. ran H ) C_ E )
16 9 2 msubf 
 |-  ( s e. ran S -> s : E --> E )
17 eqid 
 |-  ( mStat ` T ) = ( mStat ` T )
18 8 17 maxsta 
 |-  ( T e. mFS -> A C_ ( mStat ` T ) )
19 4 18 syl 
 |-  ( ph -> A C_ ( mStat ` T ) )
20 eqid 
 |-  ( mPreSt ` T ) = ( mPreSt ` T )
21 20 17 mstapst 
 |-  ( mStat ` T ) C_ ( mPreSt ` T )
22 19 21 sstrdi 
 |-  ( ph -> A C_ ( mPreSt ` T ) )
23 22 sselda 
 |-  ( ( ph /\ <. m , o , p >. e. A ) -> <. m , o , p >. e. ( mPreSt ` T ) )
24 1 2 20 elmpst 
 |-  ( <. m , o , p >. e. ( mPreSt ` T ) <-> ( ( m C_ D /\ `' m = m ) /\ ( o C_ E /\ o e. Fin ) /\ p e. E ) )
25 24 simp3bi 
 |-  ( <. m , o , p >. e. ( mPreSt ` T ) -> p e. E )
26 23 25 syl 
 |-  ( ( ph /\ <. m , o , p >. e. A ) -> p e. E )
27 ffvelrn 
 |-  ( ( s : E --> E /\ p e. E ) -> ( s ` p ) e. E )
28 16 26 27 syl2anr 
 |-  ( ( ( ph /\ <. m , o , p >. e. A ) /\ s e. ran S ) -> ( s ` p ) e. E )
29 28 a1d 
 |-  ( ( ( ph /\ <. m , o , p >. e. A ) /\ s e. ran S ) -> ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) )
30 29 ralrimiva 
 |-  ( ( ph /\ <. m , o , p >. e. A ) -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) )
31 30 ex 
 |-  ( ph -> ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) )
32 31 alrimiv 
 |-  ( ph -> A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) )
33 32 alrimivv 
 |-  ( ph -> A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) )
34 2 fvexi 
 |-  E e. _V
35 sseq2 
 |-  ( c = E -> ( ( B u. ran H ) C_ c <-> ( B u. ran H ) C_ E ) )
36 sseq2 
 |-  ( c = E -> ( ( s " ( o u. ran H ) ) C_ c <-> ( s " ( o u. ran H ) ) C_ E ) )
37 36 anbi1d 
 |-  ( c = E -> ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) <-> ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) ) )
38 eleq2 
 |-  ( c = E -> ( ( s ` p ) e. c <-> ( s ` p ) e. E ) )
39 37 38 imbi12d 
 |-  ( c = E -> ( ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) <-> ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) )
40 39 ralbidv 
 |-  ( c = E -> ( A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) <-> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) )
41 40 imbi2d 
 |-  ( c = E -> ( ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) <-> ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) ) )
42 41 albidv 
 |-  ( c = E -> ( A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) <-> A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) ) )
43 42 2albidv 
 |-  ( c = E -> ( A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) <-> A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) ) )
44 35 43 anbi12d 
 |-  ( c = E -> ( ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) <-> ( ( B u. ran H ) C_ E /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) ) ) )
45 34 44 elab 
 |-  ( E e. { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } <-> ( ( B u. ran H ) C_ E /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ E /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. E ) ) ) )
46 15 33 45 sylanbrc 
 |-  ( ph -> E e. { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
47 intss1 
 |-  ( E e. { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ E )
48 46 47 syl 
 |-  ( ph -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ E )