Theorem poimirlem4 31858

Description: Lemma for poimir 31887 connecting the admissible faces on the back face of the ( M + 1 )-cube to admissible simplices in the M-cube. (Contributed by Brendan Leahy, 21-Aug-2020.)

Hypotheses

Ref	Expression
poimir.0	|- ( ph -> N e. NN )
poimirlem4.1	|- ( ph -> K e. NN )
poimirlem4.2	|- ( ph -> M e. NN0 )
poimirlem4.3	|- ( ph -> M < N )

Assertion

Ref

Expression

poimirlem4

|- ( ph -> { s e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) | A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ~~ { s e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) | ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) ) } )

Distinct variable groups:   f, i, j, p, s   ph, j   j, M   j, N   ph, i, p, s   B, f, i, j, s   f, K, i, j, p, s   f, M, i, p, s   f, N, i, p, s

Allowed substitution hints:   ph( f)   B( p)

Proof of Theorem poimirlem4

Dummy variables k n t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . . . . . . 8 |- ( ph -> N e. NN )
2	1	adantr 466	. . . . . . 7 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> N e. NN )
3		poimirlem4.1	. . . . . . . 8 |- ( ph -> K e. NN )
4	3	adantr 466	. . . . . . 7 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> K e. NN )
5		poimirlem4.2	. . . . . . . 8 |- ( ph -> M e. NN0 )
6	5	adantr 466	. . . . . . 7 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> M e. NN0 )
7		poimirlem4.3	. . . . . . . 8 |- ( ph -> M < N )
8	7	adantr 466	. . . . . . 7 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> M < N )
9		xp1st 6834	. . . . . . . . 9 |- ( t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( 1st ` t ) e. ( ( 0..^ K ) ^m ( 1 ... M ) ) )
10		elmapi 7498	. . . . . . . . 9 |- ( ( 1st ` t ) e. ( ( 0..^ K ) ^m ( 1 ... M ) ) -> ( 1st ` t ) : ( 1 ... M ) --> ( 0..^ K ) )
11	9, 10	syl 17	. . . . . . . 8 |- ( t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( 1st ` t ) : ( 1 ... M ) --> ( 0..^ K ) )
12	11	adantl 467	. . . . . . 7 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( 1st ` t ) : ( 1 ... M ) --> ( 0..^ K ) )
13		xp2nd 6835	. . . . . . . . 9 |- ( t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( 2nd ` t ) e. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } )
14		fvex 5888	. . . . . . . . . 10 |- ( 2nd ` t ) e. _V
15		f1oeq1 5819	. . . . . . . . . 10 |- ( f = ( 2nd ` t ) -> ( f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( 2nd ` t ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
16	14, 15	elab 3218	. . . . . . . . 9 |- ( ( 2nd ` t ) e. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } <-> ( 2nd ` t ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
17	13, 16	sylib 199	. . . . . . . 8 |- ( t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( 2nd ` t ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
18	17	adantl 467	. . . . . . 7 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( 2nd ` t ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
19	2, 4, 6, 8, 12, 18	poimirlem3 31857	. . . . . 6 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B -> ( <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) ` ( M + 1 ) ) = 0 /\ ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) ` ( M + 1 ) ) = ( M + 1 ) ) ) ) )
20		fvex 5888	. . . . . . . . . . . . . . . 16 |- ( 1st ` t ) e. _V
21		snex 4659	. . . . . . . . . . . . . . . 16 |- { <. ( M + 1 ) , 0 >. } e. _V
22	20, 21	unex 6600	. . . . . . . . . . . . . . 15 |- ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) e. _V
23		snex 4659	. . . . . . . . . . . . . . . 16 |- { <. ( M + 1 ) , ( M + 1 ) >. } e. _V
24	14, 23	unex 6600	. . . . . . . . . . . . . . 15 |- ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) e. _V
25	22, 24	op1std 6814	. . . . . . . . . . . . . 14 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( 1st ` s ) = ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) )
26	22, 24	op2ndd 6815	. . . . . . . . . . . . . . . . 17 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( 2nd ` s ) = ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) )
27	26	imaeq1d 5183	. . . . . . . . . . . . . . . 16 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) )
28	27	xpeq1d 4873	. . . . . . . . . . . . . . 15 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) )
29	26	imaeq1d 5183	. . . . . . . . . . . . . . . 16 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) = ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
30	29	xpeq1d 4873	. . . . . . . . . . . . . . 15 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) = ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) )
31	28, 30	uneq12d 3621	. . . . . . . . . . . . . 14 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) )
32	25, 31	oveq12d 6320	. . . . . . . . . . . . 13 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) = ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) )
33	32	uneq1d 3619	. . . . . . . . . . . 12 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) = ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
34	33	csbeq1d 3402	. . . . . . . . . . 11 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
35	34	eqeq2d 2436	. . . . . . . . . 10 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
36	35	rexbidv 2939	. . . . . . . . 9 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
37	36	ralbidv 2864	. . . . . . . 8 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
38	25	fveq1d 5880	. . . . . . . . 9 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( 1st ` s ) ` ( M + 1 ) ) = ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) ` ( M + 1 ) ) )
39	38	eqeq1d 2424	. . . . . . . 8 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( ( 1st ` s ) ` ( M + 1 ) ) = 0 <-> ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) ` ( M + 1 ) ) = 0 ) )
40	26	fveq1d 5880	. . . . . . . . 9 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( 2nd ` s ) ` ( M + 1 ) ) = ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) ` ( M + 1 ) ) )
41	40	eqeq1d 2424	. . . . . . . 8 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) <-> ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) ` ( M + 1 ) ) = ( M + 1 ) ) )
42	37, 39, 41	3anbi123d 1335	. . . . . . 7 |- ( s = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) ) <-> ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) ` ( M + 1 ) ) = 0 /\ ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) ` ( M + 1 ) ) = ( M + 1 ) ) ) )
43	42	elrab 3229	. . . . . 6 |- ( <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. { s e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) | ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) ) } <-> ( <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) ` ( M + 1 ) ) = 0 /\ ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) ` ( M + 1 ) ) = ( M + 1 ) ) ) )
44	19, 43	syl6ibr 230	. . . . 5 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B -> <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. { s e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) | ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) ) } ) )
45	44	ralrimiva 2839	. . . 4 |- ( ph -> A. t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B -> <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. { s e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) | ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) ) } ) )
46		fveq2 5878	. . . . . . . . . . 11 |- ( s = t -> ( 1st ` s ) = ( 1st ` t ) )
47		fveq2 5878	. . . . . . . . . . . . . 14 |- ( s = t -> ( 2nd ` s ) = ( 2nd ` t ) )
48	47	imaeq1d 5183	. . . . . . . . . . . . 13 |- ( s = t -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... j ) ) )
49	48	xpeq1d 4873	. . . . . . . . . . . 12 |- ( s = t -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) )
50	47	imaeq1d 5183	. . . . . . . . . . . . 13 |- ( s = t -> ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) = ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) )
51	50	xpeq1d 4873	. . . . . . . . . . . 12 |- ( s = t -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) )
52	49, 51	uneq12d 3621	. . . . . . . . . . 11 |- ( s = t -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) )
53	46, 52	oveq12d 6320	. . . . . . . . . 10 |- ( s = t -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) )
54	53	uneq1d 3619	. . . . . . . . 9 |- ( s = t -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) = ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) )
55	54	csbeq1d 3402	. . . . . . . 8 |- ( s = t -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
56	55	eqeq2d 2436	. . . . . . 7 |- ( s = t -> ( i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
57	56	rexbidv 2939	. . . . . 6 |- ( s = t -> ( E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
58	57	ralbidv 2864	. . . . 5 |- ( s = t -> ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
59	58	ralrab 3233	. . . 4 |- ( A. t e. { s e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) | A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. { s e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) | ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) ) } <-> A. t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B -> <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. { s e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) | ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) ) } ) )
60	45, 59	sylibr 215	. . 3 |- ( ph -> A. t e. { s e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) | A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. { s e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) | ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) ) } )
61		xp1st 6834	. . . . . . . . . . . . . . 15 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( 1st ` k ) e. ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) )
62		elmapi 7498	. . . . . . . . . . . . . . 15 |- ( ( 1st ` k ) e. ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) -> ( 1st ` k ) : ( 1 ... ( M + 1 ) ) --> ( 0..^ K ) )
63	61, 62	syl 17	. . . . . . . . . . . . . 14 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( 1st ` k ) : ( 1 ... ( M + 1 ) ) --> ( 0..^ K ) )
64		fzssp1 11842	. . . . . . . . . . . . . 14 |- ( 1 ... M ) C_ ( 1 ... ( M + 1 ) )
65		fssres 5763	. . . . . . . . . . . . . 14 |- ( ( ( 1st ` k ) : ( 1 ... ( M + 1 ) ) --> ( 0..^ K ) /\ ( 1 ... M ) C_ ( 1 ... ( M + 1 ) ) ) -> ( ( 1st ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) --> ( 0..^ K ) )
66	63, 64, 65	sylancl 666	. . . . . . . . . . . . 13 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( ( 1st ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) --> ( 0..^ K ) )
67		ovex 6330	. . . . . . . . . . . . . 14 |- ( 0..^ K ) e. _V
68		ovex 6330	. . . . . . . . . . . . . 14 |- ( 1 ... M ) e. _V
69	67, 68	elmap 7505	. . . . . . . . . . . . 13 |- ( ( ( 1st ` k ) |` ( 1 ... M ) ) e. ( ( 0..^ K ) ^m ( 1 ... M ) ) <-> ( ( 1st ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) --> ( 0..^ K ) )
70	66, 69	sylibr 215	. . . . . . . . . . . 12 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( ( 1st ` k ) |` ( 1 ... M ) ) e. ( ( 0..^ K ) ^m ( 1 ... M ) ) )
71	70	ad2antlr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 1st ` k ) |` ( 1 ... M ) ) e. ( ( 0..^ K ) ^m ( 1 ... M ) ) )
72		xp2nd 6835	. . . . . . . . . . . . . . . . 17 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( 2nd ` k ) e. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } )
73		fvex 5888	. . . . . . . . . . . . . . . . . 18 |- ( 2nd ` k ) e. _V
74		f1oeq1 5819	. . . . . . . . . . . . . . . . . 18 |- ( f = ( 2nd ` k ) -> ( f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) <-> ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) ) )
75	73, 74	elab 3218	. . . . . . . . . . . . . . . . 17 |- ( ( 2nd ` k ) e. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } <-> ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) )
76	72, 75	sylib 199	. . . . . . . . . . . . . . . 16 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) )
77		f1of1 5827	. . . . . . . . . . . . . . . 16 |- ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) -> ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-> ( 1 ... ( M + 1 ) ) )
78	76, 77	syl 17	. . . . . . . . . . . . . . 15 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-> ( 1 ... ( M + 1 ) ) )
79		f1ores 5842	. . . . . . . . . . . . . . 15 |- ( ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-> ( 1 ... ( M + 1 ) ) /\ ( 1 ... M ) C_ ( 1 ... ( M + 1 ) ) ) -> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( 2nd ` k ) " ( 1 ... M ) ) )
80	78, 64, 79	sylancl 666	. . . . . . . . . . . . . 14 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( 2nd ` k ) " ( 1 ... M ) ) )
81	80	ad2antlr 731	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( 2nd ` k ) " ( 1 ... M ) ) )
82		dff1o3 5834	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) <-> ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -onto-> ( 1 ... ( M + 1 ) ) /\ Fun `' ( 2nd ` k ) ) )
83	82	simprbi 465	. . . . . . . . . . . . . . . . . 18 |- ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) -> Fun `' ( 2nd ` k ) )
84		imadif 5673	. . . . . . . . . . . . . . . . . 18 |- ( Fun `' ( 2nd ` k ) -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) \ ( ( 2nd ` k ) " { ( M + 1 ) } ) ) )
85	76, 83, 84	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) \ ( ( 2nd ` k ) " { ( M + 1 ) } ) ) )
86	85	ad2antlr 731	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) \ ( ( 2nd ` k ) " { ( M + 1 ) } ) ) )
87		f1ofo 5835	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) -> ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -onto-> ( 1 ... ( M + 1 ) ) )
88		foima 5812	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -onto-> ( 1 ... ( M + 1 ) ) -> ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) = ( 1 ... ( M + 1 ) ) )
89	76, 87, 88	3syl 18	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) = ( 1 ... ( M + 1 ) ) )
90	89	ad2antlr 731	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) = ( 1 ... ( M + 1 ) ) )
91		f1ofn 5829	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) -> ( 2nd ` k ) Fn ( 1 ... ( M + 1 ) ) )
92	76, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( 2nd ` k ) Fn ( 1 ... ( M + 1 ) ) )
93		nn0p1nn 10910	. . . . . . . . . . . . . . . . . . . . 21 |- ( M e. NN0 -> ( M + 1 ) e. NN )
94	5, 93	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( M + 1 ) e. NN )
95		elfz1end 11830	. . . . . . . . . . . . . . . . . . . 20 |- ( ( M + 1 ) e. NN <-> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
96	94, 95	sylib 199	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
97		fnsnfv 5938	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 2nd ` k ) Fn ( 1 ... ( M + 1 ) ) /\ ( M + 1 ) e. ( 1 ... ( M + 1 ) ) ) -> { ( ( 2nd ` k ) ` ( M + 1 ) ) } = ( ( 2nd ` k ) " { ( M + 1 ) } ) )
98	92, 96, 97	syl2anr 480	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) -> { ( ( 2nd ` k ) ` ( M + 1 ) ) } = ( ( 2nd ` k ) " { ( M + 1 ) } ) )
99		sneq 4006	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) -> { ( ( 2nd ` k ) ` ( M + 1 ) ) } = { ( M + 1 ) } )
100	98, 99	sylan9req 2484	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) " { ( M + 1 ) } ) = { ( M + 1 ) } )
101	90, 100	difeq12d 3584	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) \ ( ( 2nd ` k ) " { ( M + 1 ) } ) ) = ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) )
102	86, 101	eqtrd 2463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) )
103		1z 10968	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. ZZ
104		nn0uz 11194	. . . . . . . . . . . . . . . . . . . . . . 23 |- NN0 = ( ZZ>= ` 0 )
105		1m1e0 10679	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 - 1 ) = 0
106	105	fveq2i 5881	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
107	104, 106	eqtr4i 2454	. . . . . . . . . . . . . . . . . . . . . 22 |- NN0 = ( ZZ>= ` ( 1 - 1 ) )
108	5, 107	syl6eleq 2520	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M e. ( ZZ>= ` ( 1 - 1 ) ) )
109		fzsuc2 11854	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 e. ZZ /\ M e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
110	103, 108, 109	sylancr 667	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
111	110	difeq1d 3582	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( ( ( 1 ... M ) u. { ( M + 1 ) } ) \ { ( M + 1 ) } ) )
112		difun2 3875	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 1 ... M ) u. { ( M + 1 ) } ) \ { ( M + 1 ) } ) = ( ( 1 ... M ) \ { ( M + 1 ) } )
113	111, 112	syl6eq 2479	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( ( 1 ... M ) \ { ( M + 1 ) } ) )
114	5	nn0red 10927	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M e. RR )
115		ltp1 10444	. . . . . . . . . . . . . . . . . . . . . 22 |- ( M e. RR -> M < ( M + 1 ) )
116		peano2re 9807	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( M e. RR -> ( M + 1 ) e. RR )
117		ltnle 9714	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( M e. RR /\ ( M + 1 ) e. RR ) -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
118	116, 117	mpdan 672	. . . . . . . . . . . . . . . . . . . . . 22 |- ( M e. RR -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
119	115, 118	mpbid 213	. . . . . . . . . . . . . . . . . . . . 21 |- ( M e. RR -> -. ( M + 1 ) <_ M )
120	114, 119	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> -. ( M + 1 ) <_ M )
121		elfzle2 11804	. . . . . . . . . . . . . . . . . . . 20 |- ( ( M + 1 ) e. ( 1 ... M ) -> ( M + 1 ) <_ M )
122	120, 121	nsyl 124	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> -. ( M + 1 ) e. ( 1 ... M ) )
123		difsn 4131	. . . . . . . . . . . . . . . . . . 19 |- ( -. ( M + 1 ) e. ( 1 ... M ) -> ( ( 1 ... M ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
124	122, 123	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 1 ... M ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
125	113, 124	eqtrd 2463	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
126	125	imaeq2d 5184	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 2nd ` k ) " ( 1 ... M ) ) )
127	126	ad2antrr 730	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 2nd ` k ) " ( 1 ... M ) ) )
128	125	ad2antrr 730	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
129	102, 127, 128	3eqtr3d 2471	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) " ( 1 ... M ) ) = ( 1 ... M ) )
130		f1oeq3 5821	. . . . . . . . . . . . . 14 |- ( ( ( 2nd ` k ) " ( 1 ... M ) ) = ( 1 ... M ) -> ( ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( 2nd ` k ) " ( 1 ... M ) ) <-> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
131	129, 130	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( 2nd ` k ) " ( 1 ... M ) ) <-> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
132	81, 131	mpbid 213	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
133	73	resex 5164	. . . . . . . . . . . . 13 |- ( ( 2nd ` k ) |` ( 1 ... M ) ) e. _V
134		f1oeq1 5819	. . . . . . . . . . . . 13 |- ( f = ( ( 2nd ` k ) |` ( 1 ... M ) ) -> ( f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
135	133, 134	elab 3218	. . . . . . . . . . . 12 |- ( ( ( 2nd ` k ) |` ( 1 ... M ) ) e. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } <-> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
136	132, 135	sylibr 215	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( 2nd ` k ) |` ( 1 ... M ) ) e. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } )
137		opelxpi 4882	. . . . . . . . . . 11 |- ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) e. ( ( 0..^ K ) ^m ( 1 ... M ) ) /\ ( ( 2nd ` k ) |` ( 1 ... M ) ) e. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )
138	71, 136, 137	syl2anc 665	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )
139	138	3ad2antr3 1172	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) ) -> <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )
140		3anass 986	. . . . . . . . . . 11 |- ( ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) <-> ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) ) )
141		ancom 451	. . . . . . . . . . 11 |- ( ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) ) <-> ( ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) /\ A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
142	140, 141	bitri 252	. . . . . . . . . 10 |- ( ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) <-> ( ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) /\ A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
143	94	nnzd 11040	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( M + 1 ) e. ZZ )
144		uzid 11174	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( M + 1 ) e. ZZ -> ( M + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
145		peano2uz 11213	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( M + 1 ) e. ( ZZ>= ` ( M + 1 ) ) -> ( ( M + 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
146	143, 144, 145	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( ( M + 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
147	5	nn0zd 11039	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> M e. ZZ )
148	1	nnzd 11040	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> N e. ZZ )
149		zltp1le 10987	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
150		peano2z 10979	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( M e. ZZ -> ( M + 1 ) e. ZZ )
151		eluz 11173	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( M + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( M + 1 ) <_ N ) )
152	150, 151	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( M + 1 ) <_ N ) )
153	149, 152	bitr4d 259	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
154	147, 148, 153	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( M < N <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
155	7, 154	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
156		fzsplit2 11825	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( M + 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( M + 1 ) ... N ) = ( ( ( M + 1 ) ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
157	146, 155, 156	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( M + 1 ) ... N ) = ( ( ( M + 1 ) ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
158		fzsn 11841	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( M + 1 ) e. ZZ -> ( ( M + 1 ) ... ( M + 1 ) ) = { ( M + 1 ) } )
159	143, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( ( M + 1 ) ... ( M + 1 ) ) = { ( M + 1 ) } )
160	159	uneq1d 3619	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( ( M + 1 ) ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) = ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
161	157, 160	eqtrd 2463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( M + 1 ) ... N ) = ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
162	161	xpeq1d 4873	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( ( M + 1 ) ... N ) X. { 0 } ) = ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
163	162	uneq2d 3620	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) = ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
164		xpundir 4904	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) = ( ( { ( M + 1 ) } X. { 0 } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
165		ovex 6330	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M + 1 ) e. _V
166		c0ex 9638	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 e. _V
167	165, 166	xpsn 6078	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( { ( M + 1 ) } X. { 0 } ) = { <. ( M + 1 ) , 0 >. }
168	167	uneq1i 3616	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( { ( M + 1 ) } X. { 0 } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) = ( { <. ( M + 1 ) , 0 >. } u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
169	164, 168	eqtri 2451	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) = ( { <. ( M + 1 ) , 0 >. } u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
170	169	uneq2i 3617	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( { <. ( M + 1 ) , 0 >. } u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
171		unass 3623	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. { <. ( M + 1 ) , 0 >. } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) = ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( { <. ( M + 1 ) , 0 >. } u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
172	170, 171	eqtr4i 2454	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. { <. ( M + 1 ) , 0 >. } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
173	163, 172	syl6eq 2479	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) = ( ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. { <. ( M + 1 ) , 0 >. } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
174	173	ad3antrrr 734	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) = ( ( ( n e. ( 1 ... M ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. { <. ( M + 1 ) , 0 >. } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
175	165	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( M + 1 ) e. _V )
176	166	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) ) /\ j e. ( 0 ... M ) ) -> 0 e. _V )
177	110	eqcomd 2430	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( 1 ... M ) u. { ( M + 1 ) } ) = ( 1 ... ( M + 1 ) ) )
178	177	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( ( ( 0..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( 1 ... M ) u. { ( M + 1 ) } ) = ( 1 ... ( M + 1 ) ) )
179		fveq2 5878	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( M + 1 ) -> ( ( 1st ` k ) ` n ) = ( ( 1st ` k ) ` ( M + 1 ) ) )
180		fveq2 5878	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( M + 1 ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) )
181	179, 180	oveq12d 6320	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = ( M + 1 ) -> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) = ( ( ( 1st ` k ) ` ( M