Metamath Proof Explorer

Theorem mclspps

Description: The closure is closed under application of provable pre-statements. (Compare mclsax .) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclspps.d 
|- D = ( mDV ` T )
mclspps.e 
|- E = ( mEx ` T )
mclspps.c 
|- C = ( mCls ` T )
mclspps.1 
|- ( ph -> T e. mFS )
mclspps.2 
|- ( ph -> K C_ D )
mclspps.3 
|- ( ph -> B C_ E )
mclspps.j 
|- J = ( mPPSt ` T )
mclspps.l 
|- L = ( mSubst ` T )
mclspps.v 
|- V = ( mVR ` T )
mclspps.h 
|- H = ( mVH ` T )
mclspps.w 
|- W = ( mVars ` T )
mclspps.4 
|- ( ph -> <. M , O , P >. e. J )
mclspps.5 
|- ( ph -> S e. ran L )
mclspps.6 
|- ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )
mclspps.7 
|- ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )
mclspps.8 
|- ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )
Assertion mclspps 
|- ( ph -> ( S ` P ) e. ( K C B ) )

Proof

Step Hyp Ref Expression
1 mclspps.d 
 |-  D = ( mDV ` T )
2 mclspps.e 
 |-  E = ( mEx ` T )
3 mclspps.c 
 |-  C = ( mCls ` T )
4 mclspps.1 
 |-  ( ph -> T e. mFS )
5 mclspps.2 
 |-  ( ph -> K C_ D )
6 mclspps.3 
 |-  ( ph -> B C_ E )
7 mclspps.j 
 |-  J = ( mPPSt ` T )
8 mclspps.l 
 |-  L = ( mSubst ` T )
9 mclspps.v 
 |-  V = ( mVR ` T )
10 mclspps.h 
 |-  H = ( mVH ` T )
11 mclspps.w 
 |-  W = ( mVars ` T )
12 mclspps.4 
 |-  ( ph -> <. M , O , P >. e. J )
13 mclspps.5 
 |-  ( ph -> S e. ran L )
14 mclspps.6 
 |-  ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )
15 mclspps.7 
 |-  ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )
16 mclspps.8 
 |-  ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )
17 8 2 msubf 
 |-  ( S e. ran L -> S : E --> E )
18 13 17 syl 
 |-  ( ph -> S : E --> E )
19 18 ffnd 
 |-  ( ph -> S Fn E )
20 eqid 
 |-  ( mPreSt ` T ) = ( mPreSt ` T )
21 20 7 mppspst 
 |-  J C_ ( mPreSt ` T )
22 21 12 sseldi 
 |-  ( ph -> <. M , O , P >. e. ( mPreSt ` T ) )
23 1 2 20 elmpst 
 |-  ( <. M , O , P >. e. ( mPreSt ` T ) <-> ( ( M C_ D /\ `' M = M ) /\ ( O C_ E /\ O e. Fin ) /\ P e. E ) )
24 22 23 sylib 
 |-  ( ph -> ( ( M C_ D /\ `' M = M ) /\ ( O C_ E /\ O e. Fin ) /\ P e. E ) )
25 24 simp1d 
 |-  ( ph -> ( M C_ D /\ `' M = M ) )
26 25 simpld 
 |-  ( ph -> M C_ D )
27 24 simp2d 
 |-  ( ph -> ( O C_ E /\ O e. Fin ) )
28 27 simpld 
 |-  ( ph -> O C_ E )
29 eqid 
 |-  ( mAx ` T ) = ( mAx ` T )
30 14 ralrimiva 
 |-  ( ph -> A. x e. O ( S ` x ) e. ( K C B ) )
31 18 ffund 
 |-  ( ph -> Fun S )
32 18 fdmd 
 |-  ( ph -> dom S = E )
33 28 32 sseqtrrd 
 |-  ( ph -> O C_ dom S )
34 funimass5 
 |-  ( ( Fun S /\ O C_ dom S ) -> ( O C_ ( `' S " ( K C B ) ) <-> A. x e. O ( S ` x ) e. ( K C B ) ) )
35 31 33 34 syl2anc 
 |-  ( ph -> ( O C_ ( `' S " ( K C B ) ) <-> A. x e. O ( S ` x ) e. ( K C B ) ) )
36 30 35 mpbird 
 |-  ( ph -> O C_ ( `' S " ( K C B ) ) )
37 9 2 10 mvhf 
 |-  ( T e. mFS -> H : V --> E )
38 4 37 syl 
 |-  ( ph -> H : V --> E )
39 38 ffvelrnda 
 |-  ( ( ph /\ v e. V ) -> ( H ` v ) e. E )
40 elpreima 
 |-  ( S Fn E -> ( ( H ` v ) e. ( `' S " ( K C B ) ) <-> ( ( H ` v ) e. E /\ ( S ` ( H ` v ) ) e. ( K C B ) ) ) )
41 19 40 syl 
 |-  ( ph -> ( ( H ` v ) e. ( `' S " ( K C B ) ) <-> ( ( H ` v ) e. E /\ ( S ` ( H ` v ) ) e. ( K C B ) ) ) )
42 41 adantr 
 |-  ( ( ph /\ v e. V ) -> ( ( H ` v ) e. ( `' S " ( K C B ) ) <-> ( ( H ` v ) e. E /\ ( S ` ( H ` v ) ) e. ( K C B ) ) ) )
43 39 15 42 mpbir2and 
 |-  ( ( ph /\ v e. V ) -> ( H ` v ) e. ( `' S " ( K C B ) ) )
44 4 3ad2ant1 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> T e. mFS )
45 5 3ad2ant1 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> K C_ D )
46 6 3ad2ant1 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> B C_ E )
47 12 3ad2ant1 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> <. M , O , P >. e. J )
48 13 3ad2ant1 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> S e. ran L )
49 14 3ad2antl1 
 |-  ( ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) /\ x e. O ) -> ( S ` x ) e. ( K C B ) )
50 15 3ad2antl1 
 |-  ( ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )
51 16 3ad2antl1 
 |-  ( ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )
52 simp21 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> <. m , o , p >. e. ( mAx ` T ) )
53 simp22 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> s e. ran L )
54 simp23 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) )
55 simp3 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) )
56 1 2 3 44 45 46 7 8 9 10 11 47 48 49 50 51 52 53 54 55 mclsppslem 
 |-  ( ( ph /\ ( <. m , o , p >. e. ( mAx ` T ) /\ s e. ran L /\ ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) ) /\ A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) ) -> ( s ` p ) e. ( `' S " ( K C B ) ) )
57 1 2 3 4 26 28 29 8 9 10 11 36 43 56 mclsind 
 |-  ( ph -> ( M C O ) C_ ( `' S " ( K C B ) ) )
58 20 7 3 elmpps 
 |-  ( <. M , O , P >. e. J <-> ( <. M , O , P >. e. ( mPreSt ` T ) /\ P e. ( M C O ) ) )
59 58 simprbi 
 |-  ( <. M , O , P >. e. J -> P e. ( M C O ) )
60 12 59 syl 
 |-  ( ph -> P e. ( M C O ) )
61 57 60 sseldd 
 |-  ( ph -> P e. ( `' S " ( K C B ) ) )
62 elpreima 
 |-  ( S Fn E -> ( P e. ( `' S " ( K C B ) ) <-> ( P e. E /\ ( S ` P ) e. ( K C B ) ) ) )
63 62 simplbda 
 |-  ( ( S Fn E /\ P e. ( `' S " ( K C B ) ) ) -> ( S ` P ) e. ( K C B ) )
64 19 61 63 syl2anc 
 |-  ( ph -> ( S ` P ) e. ( K C B ) )