Theorem poimirlem4 32008

Description: Lemma for poimir 32037 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 472	. . . . . . 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 472	. . . . . . 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 472	. . . . . . 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 472	. . . . . . 7 |- ( ( ph /\ t e. ( ( ( 0..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> M < N )
9		xp1st 6842	. . . . . . . . 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 7511	. . . . . . . . 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 473	. . . . . . 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 6843	. . . . . . . . 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 5889	. . . . . . . . . 10 |- ( 2nd ` t ) e. _V
15		f1oeq1 5818	. . . . . . . . . 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 3173	. . . . . . . . 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 201	. . . . . . . 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 473	. . . . . . 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 32007	. . . . . 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 5889	. . . . . . . . . . . . . . . 16 |- ( 1st ` t ) e. _V
21		snex 4641	. . . . . . . . . . . . . . . 16 |- { <. ( M + 1 ) , 0 >. } e. _V
22	20, 21	unex 6608	. . . . . . . . . . . . . . 15 |- ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) e. _V
23		snex 4641	. . . . . . . . . . . . . . . 16 |- { <. ( M + 1 ) , ( M + 1 ) >. } e. _V
24	14, 23	unex 6608	. . . . . . . . . . . . . . 15 |- ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) e. _V
25	22, 24	op1std 6822	. . . . . . . . . . . . . 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 6823	. . . . . . . . . . . . . . . . 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 5173	. . . . . . . . . . . . . . . 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 4862	. . . . . . . . . . . . . . 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 5173	. . . . . . . . . . . . . . . 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 4862	. . . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . . 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 6326	. . . . . . . . . . . . 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 3578	. . . . . . . . . . . 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 3356	. . . . . . . . . . 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 2481	. . . . . . . . . 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 2892	. . . . . . . . 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 2829	. . . . . . . 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 5881	. . . . . . . . 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 2473	. . . . . . . 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 5881	. . . . . . . . 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 2473	. . . . . . . 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 1365	. . . . . . 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 3184	. . . . . 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 235	. . . . 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 2809	. . . 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 5879	. . . . . . . . . . 11 |- ( s = t -> ( 1st ` s ) = ( 1st ` t ) )
47		fveq2 5879	. . . . . . . . . . . . . 14 |- ( s = t -> ( 2nd ` s ) = ( 2nd ` t ) )
48	47	imaeq1d 5173	. . . . . . . . . . . . 13 |- ( s = t -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... j ) ) )
49	48	xpeq1d 4862	. . . . . . . . . . . 12 |- ( s = t -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) )
50	47	imaeq1d 5173	. . . . . . . . . . . . 13 |- ( s = t -> ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) = ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) )
51	50	xpeq1d 4862	. . . . . . . . . . . 12 |- ( s = t -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) )
52	49, 51	uneq12d 3580	. . . . . . . . . . 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 6326	. . . . . . . . . 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 3578	. . . . . . . . 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 3356	. . . . . . . 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 2481	. . . . . . 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 2892	. . . . . 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 2829	. . . . 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 3188	. . . 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 217	. . 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 6842	. . . . . . . . . . . . . . 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 7511	. . . . . . . . . . . . . . 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 11867	. . . . . . . . . . . . . 14 |- ( 1 ... M ) C_ ( 1 ... ( M + 1 ) )
65		fssres 5761	. . . . . . . . . . . . . 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 675	. . . . . . . . . . . . 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 6336	. . . . . . . . . . . . . 14 |- ( 0..^ K ) e. _V
68		ovex 6336	. . . . . . . . . . . . . 14 |- ( 1 ... M ) e. _V
69	67, 68	elmap 7518	. . . . . . . . . . . . 13 |- ( ( ( 1st ` k ) |` ( 1 ... M ) ) e. ( ( 0..^ K ) ^m ( 1 ... M ) ) <-> ( ( 1st ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) --> ( 0..^ K ) )
70	66, 69	sylibr 217	. . . . . . . . . . . 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 741	. . . . . . . . . . 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 6843	. . . . . . . . . . . . . . . . 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 5889	. . . . . . . . . . . . . . . . . 18 |- ( 2nd ` k ) e. _V
74		f1oeq1 5818	. . . . . . . . . . . . . . . . . 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 3173	. . . . . . . . . . . . . . . . 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 201	. . . . . . . . . . . . . . . 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 675	. . . . . . . . . . . . . 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 741	. . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . . . 18 |- ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) -> Fun `' ( 2nd ` k ) )
84		imadif 5668	. . . . . . . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . . 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 5811	. . . . . . . . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . . . 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 10933	. . . . . . . . . . . . . . . . . . . . 21 |- ( M e. NN0 -> ( M + 1 ) e. NN )
94	5, 93	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( M + 1 ) e. NN )
95		elfz1end 11855	. . . . . . . . . . . . . . . . . . . 20 |- ( ( M + 1 ) e. NN <-> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
96	94, 95	sylib 201	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
97		fnsnfv 5940	. . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . 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 3969	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) -> { ( ( 2nd ` k ) ` ( M + 1 ) ) } = { ( M + 1 ) } )
100	98, 99	sylan9req 2526	. . . . . . . . . . . . . . . . 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 3541	. . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . 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 10991	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. ZZ
104		nn0uz 11217	. . . . . . . . . . . . . . . . . . . . . . 23 |- NN0 = ( ZZ>= ` 0 )
105		1m1e0 10700	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 - 1 ) = 0
106	105	fveq2i 5882	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
107	104, 106	eqtr4i 2496	. . . . . . . . . . . . . . . . . . . . . 22 |- NN0 = ( ZZ>= ` ( 1 - 1 ) )
108	5, 107	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M e. ( ZZ>= ` ( 1 - 1 ) ) )
109		fzsuc2 11879	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 e. ZZ /\ M e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
110	103, 108, 109	sylancr 676	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
111	110	difeq1d 3539	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( ( ( 1 ... M ) u. { ( M + 1 ) } ) \ { ( M + 1 ) } ) )
112		difun2 3838	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 1 ... M ) u. { ( M + 1 ) } ) \ { ( M + 1 ) } ) = ( ( 1 ... M ) \ { ( M + 1 ) } )
113	111, 112	syl6eq 2521	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( ( 1 ... M ) \ { ( M + 1 ) } ) )
114	5	nn0red 10950	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M e. RR )
115		ltp1 10465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( M e. RR -> M < ( M + 1 ) )
116		peano2re 9824	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( M e. RR -> ( M + 1 ) e. RR )
117		ltnle 9731	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( M e. RR /\ ( M + 1 ) e. RR ) -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
118	116, 117	mpdan 681	. . . . . . . . . . . . . . . . . . . . . 22 |- ( M e. RR -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
119	115, 118	mpbid 215	. . . . . . . . . . . . . . . . . . . . 21 |- ( M e. RR -> -. ( M + 1 ) <_ M )
120	114, 119	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> -. ( M + 1 ) <_ M )
121		elfzle2 11829	. . . . . . . . . . . . . . . . . . . 20 |- ( ( M + 1 ) e. ( 1 ... M ) -> ( M + 1 ) <_ M )
122	120, 121	nsyl 125	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> -. ( M + 1 ) e. ( 1 ... M ) )
123		difsn 4097	. . . . . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
126	125	imaeq2d 5174	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 2nd ` k ) " ( 1 ... M ) ) )
127	126	ad2antrr 740	. . . . . . . . . . . . . . 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 740	. . . . . . . . . . . . . . 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 2513	. . . . . . . . . . . . . 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 5820	. . . . . . . . . . . . . 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 215	. . . . . . . . . . . 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 5154	. . . . . . . . . . . . 13 |- ( ( 2nd ` k ) |` ( 1 ... M ) ) e. _V
134		f1oeq1 5818	. . . . . . . . . . . . 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 3173	. . . . . . . . . . . 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 217	. . . . . . . . . . 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 4871	. . . . . . . . . . 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 673	. . . . . . . . . 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 1197	. . . . . . . . 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 1011	. . . . . . . . . . 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 457	. . . . . . . . . . 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 257	. . . . . . . . . 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 11062	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( M + 1 ) e. ZZ )
144		uzid 11197	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( M + 1 ) e. ZZ -> ( M + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
145		peano2uz 11235	. . . . . . . . . . . . . . . . . . . . . . . . 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 11061	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> M e. ZZ )
148	1	nnzd 11062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> N e. ZZ )
149		zltp1le 11010	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
150		peano2z 11002	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( M e. ZZ -> ( M + 1 ) e. ZZ )
151		eluz 11196	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( M + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( M + 1 ) <_ N ) )
152	150, 151	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( M + 1 ) <_ N ) )
153	149, 152	bitr4d 264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
154	147, 148, 153	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( M < N <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
155	7, 154	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
156		fzsplit2 11850	. . . . . . . . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( M + 1 ) ... N ) = ( ( ( M + 1 ) ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
158		fzsn 11866	. . . . . . . . . . . . . . . . . . . . . . . . 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 3578	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( ( M + 1 ) ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) = ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
161	157, 160	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( M + 1 ) ... N ) = ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
162	161	xpeq1d 4862	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( ( M + 1 ) ... N ) X. { 0 } ) = ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
163	162	uneq2d 3579	. . . . . . . . . . . . . . . . . . . 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 4893	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) = ( ( { ( M + 1 ) } X. { 0 } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
165		ovex 6336	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M + 1 ) e. _V
166		c0ex 9655	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 e. _V
167	165, 166	xpsn 6082	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( { ( M + 1 ) } X. { 0 } ) = { <. ( M + 1 ) , 0 >. }
168	167	uneq1i 3575	. . . . . . . . . . . . . . . . . . . . . . 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 2493	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) = ( { <. ( M + 1 ) , 0 >. } u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
170	169	uneq2i 3576	. . . . . . . . . . . . . . . . . . . . 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 3582	. . . . . . . . . . . . . . . . . . . . 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 2496	. . . . . . . . . . . . . . . . . . . 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 2521	. . . . . . . . . . . . . . . . . . 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 744	. . . . . . . . . . . . . . . . . 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 2477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( 1 ... M ) u. { ( M + 1 ) } ) = ( 1 ... ( M + 1 ) ) )
178	177	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( M + 1 ) -> ( ( 1st ` k ) ` n ) = ( ( 1st ` k ) ` ( M + 1 ) ) )
180		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . 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 6326	. . . . . . . . . . . . . . . . . . . . 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 ) `