Theorem mclsppslem 30173

Description: The closure is closed under application of provable pre-statements. (Compare mclsax 30159.) 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.)

Hypotheses

Ref	Expression
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 )
mclsppslem.9	|- ( ph -> <. m , o , p >. e. (mAx ` T ) )
mclsppslem.10	|- ( ph -> s e. ran L )
mclsppslem.11	|- ( ph -> ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) )
mclsppslem.12	|- ( ph -> A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) )

Assertion

Ref	Expression
mclsppslem	|- ( ph -> ( s ` p ) e. ( `' S " ( K C B ) ) )

Distinct variable groups:   m, o, p, s, v, E   a, b, m, o, p, s, v, w, x, y, z, H   v, V, z   K, a, b, m, o, p, s, v, x, y   T, a, b, m, o, p, s, v, w, x, y, z   L, a, b, m, o, p, s, v, w, x, y, z   S, a, b, m, o, p, s, v, x, y   B, a, b, m, o, p, s, v, x, y   W, a, b, m, o, p, s, v, w, x, y, z   C, a, b, m, o, p, s, v, x, y, z   M, a, b, m, o, p, s, v, w, x, y, z   m, O, o, p, s, v, w, x, z   ph, a, b, v, x, y

Allowed substitution hints:   ph( z, w, m, o, s, p)   B( z, w)   C( w)   D( x, y, z, w, v, m, o, s, p, a, b)   P( x, y, z, w, v, m, o, s, p, a, b)   S( z, w)   E( x, y, z, w, a, b)   J( x, y, z, w, v, m, o, s, p, a, b)   K( z, w)   O( y, a, b)   V( x, y, w, m, o, s, p, a, b)

Proof of Theorem mclsppslem

Dummy variables t u c d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mclsppslem.10	. . . 4 |- ( ph -> s e. ran L )
2		mclspps.l	. . . . 5 |- L = (mSubst ` T )
3		mclspps.e	. . . . 5 |- E = (mEx ` T )
4	2, 3	msubf 30122	. . . 4 |- ( s e. ran L -> s : E --> E )
5	1, 4	syl 17	. . 3 |- ( ph -> s : E --> E )
6		mclspps.1	. . . . . . . 8 |- ( ph -> T e. mFS )
7		eqid 2428	. . . . . . . . 9 |- (mAx ` T ) = (mAx ` T )
8		eqid 2428	. . . . . . . . 9 |- (mStat ` T ) = (mStat ` T )
9	7, 8	maxsta 30144	. . . . . . . 8 |- ( T e. mFS -> (mAx ` T ) C_ (mStat ` T ) )
10	6, 9	syl 17	. . . . . . 7 |- ( ph -> (mAx ` T ) C_ (mStat ` T ) )
11		eqid 2428	. . . . . . . 8 |- (mPreSt ` T ) = (mPreSt ` T )
12	11, 8	mstapst 30137	. . . . . . 7 |- (mStat ` T ) C_ (mPreSt ` T )
13	10, 12	syl6ss 3419	. . . . . 6 |- ( ph -> (mAx ` T ) C_ (mPreSt ` T ) )
14		mclsppslem.9	. . . . . 6 |- ( ph -> <. m , o , p >. e. (mAx ` T ) )
15	13, 14	sseldd 3408	. . . . 5 |- ( ph -> <. m , o , p >. e. (mPreSt ` T ) )
16		mclspps.d	. . . . . 6 |- D = (mDV ` T )
17	16, 3, 11	elmpst 30126	. . . . 5 |- ( <. m , o , p >. e. (mPreSt ` T ) <-> ( ( m C_ D /\ `' m = m ) /\ ( o C_ E /\ o e. Fin ) /\ p e. E ) )
18	15, 17	sylib 199	. . . 4 |- ( ph -> ( ( m C_ D /\ `' m = m ) /\ ( o C_ E /\ o e. Fin ) /\ p e. E ) )
19	18	simp3d 1019	. . 3 |- ( ph -> p e. E )
20	5, 19	ffvelrnd 5982	. 2 |- ( ph -> ( s ` p ) e. E )
21		fvco3 5902	. . . 4 |- ( ( s : E --> E /\ p e. E ) -> ( ( S o. s ) ` p ) = ( S ` ( s ` p ) ) )
22	5, 19, 21	syl2anc 665	. . 3 |- ( ph -> ( ( S o. s ) ` p ) = ( S ` ( s ` p ) ) )
23		mclspps.c	. . . 4 |- C = (mCls ` T )
24		mclspps.2	. . . 4 |- ( ph -> K C_ D )
25		mclspps.3	. . . 4 |- ( ph -> B C_ E )
26		mclspps.v	. . . 4 |- V = (mVR ` T )
27		mclspps.h	. . . 4 |- H = (mVH ` T )
28		mclspps.w	. . . 4 |- W = (mVars ` T )
29		mclspps.5	. . . . 5 |- ( ph -> S e. ran L )
30	2	msubco 30121	. . . . 5 |- ( ( S e. ran L /\ s e. ran L ) -> ( S o. s ) e. ran L )
31	29, 1, 30	syl2anc 665	. . . 4 |- ( ph -> ( S o. s ) e. ran L )
32	2, 3	msubf 30122	. . . . . . . . 9 |- ( S e. ran L -> S : E --> E )
33	29, 32	syl 17	. . . . . . . 8 |- ( ph -> S : E --> E )
34		fco 5699	. . . . . . . 8 |- ( ( S : E --> E /\ s : E --> E ) -> ( S o. s ) : E --> E )
35	33, 5, 34	syl2anc 665	. . . . . . 7 |- ( ph -> ( S o. s ) : E --> E )
36		ffn 5689	. . . . . . 7 |- ( ( S o. s ) : E --> E -> ( S o. s ) Fn E )
37	35, 36	syl 17	. . . . . 6 |- ( ph -> ( S o. s ) Fn E )
38	37	adantr 466	. . . . 5 |- ( ( ph /\ c e. o ) -> ( S o. s ) Fn E )
39		mclsppslem.11	. . . . . . . . 9 |- ( ph -> ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) )
40		ffun 5691	. . . . . . . . . . 11 |- ( s : E --> E -> Fun s )
41	5, 40	syl 17	. . . . . . . . . 10 |- ( ph -> Fun s )
42	17	simp2bi 1021	. . . . . . . . . . . . . 14 |- ( <. m , o , p >. e. (mPreSt ` T ) -> ( o C_ E /\ o e. Fin ) )
43	15, 42	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( o C_ E /\ o e. Fin ) )
44	43	simpld 460	. . . . . . . . . . . 12 |- ( ph -> o C_ E )
45	26, 3, 27	mvhf 30148	. . . . . . . . . . . . 13 |- ( T e. mFS -> H : V --> E )
46		frn 5695	. . . . . . . . . . . . 13 |- ( H : V --> E -> ran H C_ E )
47	6, 45, 46	3syl 18	. . . . . . . . . . . 12 |- ( ph -> ran H C_ E )
48	44, 47	unssd 3585	. . . . . . . . . . 11 |- ( ph -> ( o u. ran H ) C_ E )
49		fdm 5693	. . . . . . . . . . . 12 |- ( s : E --> E -> dom s = E )
50	5, 49	syl 17	. . . . . . . . . . 11 |- ( ph -> dom s = E )
51	48, 50	sseqtr4d 3444	. . . . . . . . . 10 |- ( ph -> ( o u. ran H ) C_ dom s )
52		funimass3 5957	. . . . . . . . . 10 |- ( ( Fun s /\ ( o u. ran H ) C_ dom s ) -> ( ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) <-> ( o u. ran H ) C_ ( `' s " ( `' S " ( K C B ) ) ) ) )
53	41, 51, 52	syl2anc 665	. . . . . . . . 9 |- ( ph -> ( ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) <-> ( o u. ran H ) C_ ( `' s " ( `' S " ( K C B ) ) ) ) )
54	39, 53	mpbid 213	. . . . . . . 8 |- ( ph -> ( o u. ran H ) C_ ( `' s " ( `' S " ( K C B ) ) ) )
55		cnvco 4982	. . . . . . . . . 10 |- `' ( S o. s ) = ( `' s o. `' S )
56	55	imaeq1i 5127	. . . . . . . . 9 |- ( `' ( S o. s ) " ( K C B ) ) = ( ( `' s o. `' S ) " ( K C B ) )
57		imaco 5302	. . . . . . . . 9 |- ( ( `' s o. `' S ) " ( K C B ) ) = ( `' s " ( `' S " ( K C B ) ) )
58	56, 57	eqtri 2450	. . . . . . . 8 |- ( `' ( S o. s ) " ( K C B ) ) = ( `' s " ( `' S " ( K C B ) ) )
59	54, 58	syl6sseqr 3454	. . . . . . 7 |- ( ph -> ( o u. ran H ) C_ ( `' ( S o. s ) " ( K C B ) ) )
60	59	unssad 3586	. . . . . 6 |- ( ph -> o C_ ( `' ( S o. s ) " ( K C B ) ) )
61	60	sselda 3407	. . . . 5 |- ( ( ph /\ c e. o ) -> c e. ( `' ( S o. s ) " ( K C B ) ) )
62		elpreima 5961	. . . . . 6 |- ( ( S o. s ) Fn E -> ( c e. ( `' ( S o. s ) " ( K C B ) ) <-> ( c e. E /\ ( ( S o. s ) ` c ) e. ( K C B ) ) ) )
63	62	simplbda 628	. . . . 5 |- ( ( ( S o. s ) Fn E /\ c e. ( `' ( S o. s ) " ( K C B ) ) ) -> ( ( S o. s ) ` c ) e. ( K C B ) )
64	38, 61, 63	syl2anc 665	. . . 4 |- ( ( ph /\ c e. o ) -> ( ( S o. s ) ` c ) e. ( K C B ) )
65	37	adantr 466	. . . . 5 |- ( ( ph /\ t e. V ) -> ( S o. s ) Fn E )
66	59	unssbd 3587	. . . . . . 7 |- ( ph -> ran H C_ ( `' ( S o. s ) " ( K C B ) ) )
67	66	adantr 466	. . . . . 6 |- ( ( ph /\ t e. V ) -> ran H C_ ( `' ( S o. s ) " ( K C B ) ) )
68		ffn 5689	. . . . . . . 8 |- ( H : V --> E -> H Fn V )
69	6, 45, 68	3syl 18	. . . . . . 7 |- ( ph -> H Fn V )
70		fnfvelrn 5978	. . . . . . 7 |- ( ( H Fn V /\ t e. V ) -> ( H ` t ) e. ran H )
71	69, 70	sylan 473	. . . . . 6 |- ( ( ph /\ t e. V ) -> ( H ` t ) e. ran H )
72	67, 71	sseldd 3408	. . . . 5 |- ( ( ph /\ t e. V ) -> ( H ` t ) e. ( `' ( S o. s ) " ( K C B ) ) )
73		elpreima 5961	. . . . . 6 |- ( ( S o. s ) Fn E -> ( ( H ` t ) e. ( `' ( S o. s ) " ( K C B ) ) <-> ( ( H ` t ) e. E /\ ( ( S o. s ) ` ( H ` t ) ) e. ( K C B ) ) ) )
74	73	simplbda 628	. . . . 5 |- ( ( ( S o. s ) Fn E /\ ( H ` t ) e. ( `' ( S o. s ) " ( K C B ) ) ) -> ( ( S o. s ) ` ( H ` t ) ) e. ( K C B ) )
75	65, 72, 74	syl2anc 665	. . . 4 |- ( ( ph /\ t e. V ) -> ( ( S o. s ) ` ( H ` t ) ) e. ( K C B ) )
76	5	adantr 466	. . . . . . . . . . . . 13 |- ( ( ph /\ c m d ) -> s : E --> E )
77	6, 45	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> H : V --> E )
78	77	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ c m d ) -> H : V --> E )
79	18	simp1d 1017	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( m C_ D /\ `' m = m ) )
80	79	simpld 460	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> m C_ D )
81	26, 16	mdvval 30094	. . . . . . . . . . . . . . . . . . . 20 |- D = ( ( V X. V ) \ _I )
82		difss 3535	. . . . . . . . . . . . . . . . . . . 20 |- ( ( V X. V ) \ _I ) C_ ( V X. V )
83	81, 82	eqsstri 3437	. . . . . . . . . . . . . . . . . . 19 |- D C_ ( V X. V )
84	80, 83	syl6ss 3419	. . . . . . . . . . . . . . . . . 18 |- ( ph -> m C_ ( V X. V ) )
85	84	ssbrd 4408	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( c m d -> c ( V X. V ) d ) )
86	85	imp 430	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c m d ) -> c ( V X. V ) d )
87		brxp 4827	. . . . . . . . . . . . . . . 16 |- ( c ( V X. V ) d <-> ( c e. V /\ d e. V ) )
88	86, 87	sylib 199	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c m d ) -> ( c e. V /\ d e. V ) )
89	88	simpld 460	. . . . . . . . . . . . . 14 |- ( ( ph /\ c m d ) -> c e. V )
90	78, 89	ffvelrnd 5982	. . . . . . . . . . . . 13 |- ( ( ph /\ c m d ) -> ( H ` c ) e. E )
91		fvco3 5902	. . . . . . . . . . . . 13 |- ( ( s : E --> E /\ ( H ` c ) e. E ) -> ( ( S o. s ) ` ( H ` c ) ) = ( S ` ( s ` ( H ` c ) ) ) )
92	76, 90, 91	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ph /\ c m d ) -> ( ( S o. s ) ` ( H ` c ) ) = ( S ` ( s ` ( H ` c ) ) ) )
93	92	fveq2d 5829	. . . . . . . . . . 11 |- ( ( ph /\ c m d ) -> ( W ` ( ( S o. s ) ` ( H ` c ) ) ) = ( W ` ( S ` ( s ` ( H ` c ) ) ) ) )
94	6	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ c m d ) -> T e. mFS )
95	29	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ c m d ) -> S e. ran L )
96	76, 90	ffvelrnd 5982	. . . . . . . . . . . 12 |- ( ( ph /\ c m d ) -> ( s ` ( H ` c ) ) e. E )
97	2, 3, 28, 27	msubvrs 30150	. . . . . . . . . . . 12 |- ( ( T e. mFS /\ S e. ran L /\ ( s ` ( H ` c ) ) e. E ) -> ( W ` ( S ` ( s ` ( H ` c ) ) ) ) = U_ u e. ( W ` ( s ` ( H ` c ) ) ) ( W ` ( S ` ( H ` u ) ) ) )
98	94, 95, 96, 97	syl3anc 1264	. . . . . . . . . . 11 |- ( ( ph /\ c m d ) -> ( W ` ( S ` ( s ` ( H ` c ) ) ) ) = U_ u e. ( W ` ( s ` ( H ` c ) ) ) ( W ` ( S ` ( H ` u ) ) ) )
99	93, 98	eqtrd 2462	. . . . . . . . . 10 |- ( ( ph /\ c m d ) -> ( W ` ( ( S o. s ) ` ( H ` c ) ) ) = U_ u e. ( W ` ( s ` ( H ` c ) ) ) ( W ` ( S ` ( H ` u ) ) ) )
100	99	eleq2d 2491	. . . . . . . . 9 |- ( ( ph /\ c m d ) -> ( a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) <-> a e. U_ u e. ( W ` ( s ` ( H ` c ) ) ) ( W ` ( S ` ( H ` u ) ) ) ) )
101		eliun 4247	. . . . . . . . 9 |- ( a e. U_ u e. ( W ` ( s ` ( H ` c ) ) ) ( W ` ( S ` ( H ` u ) ) ) <-> E. u e. ( W ` ( s ` ( H ` c ) ) ) a e. ( W ` ( S ` ( H ` u ) ) ) )
102	100, 101	syl6bb 264	. . . . . . . 8 |- ( ( ph /\ c m d ) -> ( a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) <-> E. u e. ( W ` ( s ` ( H ` c ) ) ) a e. ( W ` ( S ` ( H ` u ) ) ) ) )
103	88	simprd 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ c m d ) -> d e. V )
104	78, 103	ffvelrnd 5982	. . . . . . . . . . . . 13 |- ( ( ph /\ c m d ) -> ( H ` d ) e. E )
105		fvco3 5902	. . . . . . . . . . . . 13 |- ( ( s : E --> E /\ ( H ` d ) e. E ) -> ( ( S o. s ) ` ( H ` d ) ) = ( S ` ( s ` ( H ` d ) ) ) )
106	76, 104, 105	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ph /\ c m d ) -> ( ( S o. s ) ` ( H ` d ) ) = ( S ` ( s ` ( H ` d ) ) ) )
107	106	fveq2d 5829	. . . . . . . . . . 11 |- ( ( ph /\ c m d ) -> ( W ` ( ( S o. s ) ` ( H ` d ) ) ) = ( W ` ( S ` ( s ` ( H ` d ) ) ) ) )
108	76, 104	ffvelrnd 5982	. . . . . . . . . . . 12 |- ( ( ph /\ c m d ) -> ( s ` ( H ` d ) ) e. E )
109	2, 3, 28, 27	msubvrs 30150	. . . . . . . . . . . 12 |- ( ( T e. mFS /\ S e. ran L /\ ( s ` ( H ` d ) ) e. E ) -> ( W ` ( S ` ( s ` ( H ` d ) ) ) ) = U_ v e. ( W ` ( s ` ( H ` d ) ) ) ( W ` ( S ` ( H ` v ) ) ) )
110	94, 95, 108, 109	syl3anc 1264	. . . . . . . . . . 11 |- ( ( ph /\ c m d ) -> ( W ` ( S ` ( s ` ( H ` d ) ) ) ) = U_ v e. ( W ` ( s ` ( H ` d ) ) ) ( W ` ( S ` ( H ` v ) ) ) )
111	107, 110	eqtrd 2462	. . . . . . . . . 10 |- ( ( ph /\ c m d ) -> ( W ` ( ( S o. s ) ` ( H ` d ) ) ) = U_ v e. ( W ` ( s ` ( H ` d ) ) ) ( W ` ( S ` ( H ` v ) ) ) )
112	111	eleq2d 2491	. . . . . . . . 9 |- ( ( ph /\ c m d ) -> ( b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) <-> b e. U_ v e. ( W ` ( s ` ( H ` d ) ) ) ( W ` ( S ` ( H ` v ) ) ) ) )
113		eliun 4247	. . . . . . . . 9 |- ( b e. U_ v e. ( W ` ( s ` ( H ` d ) ) ) ( W ` ( S ` ( H ` v ) ) ) <-> E. v e. ( W ` ( s ` ( H ` d ) ) ) b e. ( W ` ( S ` ( H ` v ) ) ) )
114	112, 113	syl6bb 264	. . . . . . . 8 |- ( ( ph /\ c m d ) -> ( b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) <-> E. v e. ( W ` ( s ` ( H ` d ) ) ) b e. ( W ` ( S ` ( H ` v ) ) ) ) )
115	102, 114	anbi12d 715	. . . . . . 7 |- ( ( ph /\ c m d ) -> ( ( a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) /\ b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) ) <-> ( E. u e. ( W ` ( s ` ( H ` c ) ) ) a e. ( W ` ( S ` ( H ` u ) ) ) /\ E. v e. ( W ` ( s ` ( H ` d ) ) ) b e. ( W ` ( S ` ( H ` v ) ) ) ) ) )
116		reeanv 2935	. . . . . . . 8 |- ( E. u e. ( W ` ( s ` ( H ` c ) ) ) E. v e. ( W ` ( s ` ( H ` d ) ) ) ( a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) <-> ( E. u e. ( W ` ( s ` ( H ` c ) ) ) a e. ( W ` ( S ` ( H ` u ) ) ) /\ E. v e. ( W ` ( s ` ( H ` d ) ) ) b e. ( W ` ( S ` ( H ` v ) ) ) ) )
117		simpll 758	. . . . . . . . . 10 |- ( ( ( ph /\ c m d ) /\ ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) ) -> ph )
118		brxp 4827	. . . . . . . . . . . 12 |- ( u ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) v <-> ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) )
119		mclsppslem.12	. . . . . . . . . . . . . . 15 |- ( ph -> A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) )
120		vex 3025	. . . . . . . . . . . . . . . 16 |- c e. _V
121		vex 3025	. . . . . . . . . . . . . . . 16 |- d e. _V
122		breq12 4371	. . . . . . . . . . . . . . . . . 18 |- ( ( z = c /\ w = d ) -> ( z m w <-> c m d ) )
123		simpl 458	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( z = c /\ w = d ) -> z = c )
124	123	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( z = c /\ w = d ) -> ( H ` z ) = ( H ` c ) )
125	124	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z = c /\ w = d ) -> ( s ` ( H ` z ) ) = ( s ` ( H ` c ) ) )
126	125	fveq2d 5829	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z = c /\ w = d ) -> ( W ` ( s ` ( H ` z ) ) ) = ( W ` ( s ` ( H ` c ) ) ) )
127		simpr 462	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( z = c /\ w = d ) -> w = d )
128	127	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( z = c /\ w = d ) -> ( H ` w ) = ( H ` d ) )
129	128	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z = c /\ w = d ) -> ( s ` ( H ` w ) ) = ( s ` ( H ` d ) ) )
130	129	fveq2d 5829	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z = c /\ w = d ) -> ( W ` ( s ` ( H ` w ) ) ) = ( W ` ( s ` ( H ` d ) ) ) )
131	126, 130	xpeq12d 4821	. . . . . . . . . . . . . . . . . . 19 |- ( ( z = c /\ w = d ) -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) = ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) )
132	131	sseq1d 3434	. . . . . . . . . . . . . . . . . 18 |- ( ( z = c /\ w = d ) -> ( ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M <-> ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) C_ M ) )
133	122, 132	imbi12d 321	. . . . . . . . . . . . . . . . 17 |- ( ( z = c /\ w = d ) -> ( ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) <-> ( c m d -> ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) C_ M ) ) )
134	133	spc2gv 3112	. . . . . . . . . . . . . . . 16 |- ( ( c e. _V /\ d e. _V ) -> ( A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) -> ( c m d -> ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) C_ M ) ) )
135	120, 121, 134	mp2an 676	. . . . . . . . . . . . . . 15 |- ( A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) -> ( c m d -> ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) C_ M ) )
136	119, 135	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( c m d -> ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) C_ M ) )
137	136	imp 430	. . . . . . . . . . . . 13 |- ( ( ph /\ c m d ) -> ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) C_ M )
138	137	ssbrd 4408	. . . . . . . . . . . 12 |- ( ( ph /\ c m d ) -> ( u ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) v -> u M v ) )
139	118, 138	syl5bir 221	. . . . . . . . . . 11 |- ( ( ph /\ c m d ) -> ( ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) -> u M v ) )
140	139	imp 430	. . . . . . . . . 10 |- ( ( ( ph /\ c m d ) /\ ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) ) -> u M v )
141		vex 3025	. . . . . . . . . . . . 13 |- u e. _V
142		vex 3025	. . . . . . . . . . . . 13 |- v e. _V
143		breq12 4371	. . . . . . . . . . . . . . . 16 |- ( ( x = u /\ y = v ) -> ( x M y <-> u M v ) )
144		simpl 458	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = u /\ y = v ) -> x = u )
145	144	fveq2d 5829	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = u /\ y = v ) -> ( H ` x ) = ( H ` u ) )
146	145	fveq2d 5829	. . . . . . . . . . . . . . . . . 18 |- ( ( x = u /\ y = v ) -> ( S ` ( H ` x ) ) = ( S ` ( H ` u ) ) )
147	146	fveq2d 5829	. . . . . . . . . . . . . . . . 17 |- ( ( x = u /\ y = v ) -> ( W ` ( S ` ( H ` x ) ) ) = ( W ` ( S ` ( H ` u ) ) ) )
148	147	eleq2d 2491	. . . . . . . . . . . . . . . 16 |- ( ( x = u /\ y = v ) -> ( a e. ( W ` ( S ` ( H ` x ) ) ) <-> a e. ( W ` ( S ` ( H ` u ) ) ) ) )
149		simpr 462	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = u /\ y = v ) -> y = v )
150	149	fveq2d 5829	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = u /\ y = v ) -> ( H ` y ) = ( H ` v ) )
151	150	fveq2d 5829	. . . . . . . . . . . . . . . . . 18 |- ( ( x = u /\ y = v ) -> ( S ` ( H ` y ) ) = ( S ` ( H ` v ) ) )
152	151	fveq2d 5829	. . . . . . . . . . . . . . . . 17 |- ( ( x = u /\ y = v ) -> ( W ` ( S ` ( H ` y ) ) ) = ( W ` ( S ` ( H ` v ) ) ) )
153	152	eleq2d 2491	. . . . . . . . . . . . . . . 16 |- ( ( x = u /\ y = v ) -> ( b e. ( W ` ( S ` ( H ` y ) ) ) <-> b e. ( W ` ( S ` ( H ` v ) ) ) ) )
154	143, 148, 153	3anbi123d 1335	. . . . . . . . . . . . . . 15 |- ( ( x = u /\ y = v ) -> ( ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) <-> ( u M v /\ a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) ) )
155	154	anbi2d 708	. . . . . . . . . . . . . 14 |- ( ( x = u /\ y = v ) -> ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) <-> ( ph /\ ( u M v /\ a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) ) ) )
156	155	imbi1d 318	. . . . . . . . . . . . 13 |- ( ( x = u /\ y = v ) -> ( ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b ) <-> ( ( ph /\ ( u M v /\ a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) ) -> a K b ) ) )
157		mclspps.8	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )
158	141, 142, 156, 157	vtocl2 3077	. . . . . . . . . . . 12 |- ( ( ph /\ ( u M v /\ a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) ) -> a K b )
159	158	3exp2 1223	. . . . . . . . . . 11 |- ( ph -> ( u M v -> ( a e. ( W ` ( S ` ( H ` u ) ) ) -> ( b e. ( W ` ( S ` ( H ` v ) ) ) -> a K b ) ) ) )
160	159	imp4b 593	. . . . . . . . . 10 |- ( ( ph /\ u M v ) -> ( ( a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) -> a K b ) )
161	117, 140, 160	syl2anc 665	. . . . . . . . 9 |- ( ( ( ph /\ c m d ) /\ ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) ) -> ( ( a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) -> a K b ) )
162	161	rexlimdvva 2863	. . . . . . . 8 |- ( ( ph /\ c m d ) -> ( E. u e. ( W ` ( s ` ( H ` c ) ) ) E. v e. ( W ` ( s ` ( H ` d ) ) ) ( a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) -> a K b ) )
163	116, 162	syl5bir 221	. . . . . . 7 |- ( ( ph /\ c m d ) -> ( ( E. u e. ( W ` ( s ` ( H ` c ) ) ) a e. ( W ` ( S ` ( H ` u ) ) ) /\ E. v e. ( W ` ( s ` ( H ` d ) ) ) b e. ( W ` ( S ` ( H ` v ) ) ) ) -> a K b ) )
164	115, 163	sylbid 218	. . . . . 6 |- ( ( ph /\ c m d ) -> ( ( a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) /\ b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) ) -> a K b ) )
165	164	exp4b 610	. . . . 5 |- ( ph -> ( c m d -> ( a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) -> ( b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) -> a K b ) ) ) )
166	165	3imp2 1220	. . . 4 |- ( ( ph /\ ( c m d /\ a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) /\ b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) ) ) -> a K b )
167	16, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 64, 75, 166	mclsax 30159	. . 3 |- ( ph -> ( ( S o. s ) ` p ) e. ( K C B ) )
168	22, 167	eqeltrrd 2507	. 2 |- ( ph -> ( S ` ( s ` p ) ) e. ( K C B ) )
169		ffn 5689	. . . 4 |- ( S : E --> E -> S Fn E )
170	33, 169	syl 17	. . 3 |- ( ph -> S Fn E )
171		elpreima 5961	. . 3 |- ( S Fn E -> ( ( s ` p ) e. ( `' S " ( K C B ) ) <-> ( ( s ` p ) e. E /\ ( S ` ( s ` p ) ) e. ( K C B ) ) ) )
172	170, 171	syl 17	. 2 |- ( ph -> ( ( s ` p ) e. ( `' S " ( K C B ) ) <-> ( ( s ` p ) e. E /\ ( S ` ( s ` p ) ) e. ( K C B ) ) ) )
173	20, 168, 172	mpbir2and 930	1 |- ( ph -> ( s ` p ) e. ( `' S " ( K C B ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   A.wal 1435   = wceq 1437   e. wcel 1872   E.wrex 2715   _Vcvv 3022   \ cdif 3376   u. cun 3377   C_ wss 3379   <.cotp 3949   U_ciun 4242   class class class wbr 4366   _I cid 4706   X. cxp 4794   `'ccnv 4795   dom cdm 4796   ran crn 4797   "cima 4799   o. ccom 4800   Fun wfun 5538   Fn wfn 5539   -->wf 5540   ` cfv 5544  (class class class)co 6249   Fincfn 7524  mVRcmvar 30051  mAxcmax 30055  mExcmex 30057  mDVcmdv 30058  mVarscmvrs 30059  mSubstcmsub 30061  mVHcmvh 30062  mPreStcmpst 30063  mStatcmsta 30065  mFScmfs 30066  mClscmcls 30067  mPPStcmpps 30068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-ot 3950  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-map 7429  df-pm 7430  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-card 8325  df-cda 8549  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-2 10619  df-n0 10821  df-z 10889  df-uz 11111  df-fz 11736  df-fzo 11867  df-seq 12164  df-hash 12466  df-word 12612  df-lsw 12613  df-concat 12614  df-s1 12615  df-substr 12616  df-struct 15066  df-ndx 15067  df-slot 15068  df-base 15069  df-sets 15070  df-ress 15071  df-plusg 15146  df-0g 15283  df-gsum 15284  df-mgm 16431  df-sgrp 16470  df-mnd 16480  df-mhm 16525  df-submnd 16526  df-frmd 16576  df-vrmd 16577  df-mrex 30076  df-mex 30077  df-mdv 30078  df-mvrs 30079  df-mrsub 30080  df-msub 30081  df-mvh 30082  df-mpst 30083  df-msr 30084  df-msta 30085  df-mfs 30086  df-mcls 30087

This theorem is referenced by:  mclspps  30174