Metamath Proof Explorer

Theorem poimirlem4

Description: Lemma for poimir 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)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem4.1 
|- ( ph -> K e. NN )
poimirlem4.2 
|- ( ph -> M e. NN0 )
poimirlem4.3 
|- ( ph -> M < N )
Assertion 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 ) ) } )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem4.1 
 |-  ( ph -> K e. NN )
3 poimirlem4.2 
 |-  ( ph -> M e. NN0 )
4 poimirlem4.3 
 |-  ( ph -> M < N )
5 1 adantr 
 |-  ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> N e. NN )
6 2 adantr 
 |-  ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> K e. NN )
7 3 adantr 
 |-  ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> M e. NN0 )
8 4 adantr 
 |-  ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> M < N )
9 xp1st 
 |-  ( 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 
 |-  ( ( 1st ` t ) e. ( ( 0 ..^ K ) ^m ( 1 ... M ) ) -> ( 1st ` t ) : ( 1 ... M ) --> ( 0 ..^ K ) )
11 9 10 syl 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( 2nd ` t ) e. _V
15 f1oeq1 
 |-  ( f = ( 2nd ` t ) -> ( f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( 2nd ` t ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
16 14 15 elab 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( 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 5 6 7 8 12 18 poimirlem3 
 |-  ( ( 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 
 |-  ( 1st ` t ) e. _V
21 snex 
 |-  { <. ( M + 1 ) , 0 >. } e. _V
22 20 21 unex 
 |-  ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) e. _V
23 snex 
 |-  { <. ( M + 1 ) , ( M + 1 ) >. } e. _V
24 14 23 unex 
 |-  ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) e. _V
25 22 24 op1std 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( <. ( ( 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 imbitrrdi 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( s = t -> ( 1st ` s ) = ( 1st ` t ) )
47 fveq2 
 |-  ( s = t -> ( 2nd ` s ) = ( 2nd ` t ) )
48 47 imaeq1d 
 |-  ( s = t -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... j ) ) )
49 48 xpeq1d 
 |-  ( s = t -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) )
50 47 imaeq1d 
 |-  ( s = t -> ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) = ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) )
51 50 xpeq1d 
 |-  ( s = t -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) )
52 49 51 uneq12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( 1st ` k ) e. ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) -> ( 1st ` k ) : ( 1 ... ( M + 1 ) ) --> ( 0 ..^ K ) )
63 61 62 syl 
 |-  ( 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 
 |-  ( 1 ... M ) C_ ( 1 ... ( M + 1 ) )
65 fssres 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  ( 0 ..^ K ) e. _V
68 ovex 
 |-  ( 1 ... M ) e. _V
69 67 68 elmap 
 |-  ( ( ( 1st ` k ) |` ( 1 ... M ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... M ) ) <-> ( ( 1st ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) --> ( 0 ..^ K ) )
70 66 69 sylibr 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  ( 2nd ` k ) e. _V
74 f1oeq1 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) -> Fun `' ( 2nd ` k ) )
84 imadif 
 |-  ( Fun `' ( 2nd ` k ) -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) \ ( ( 2nd ` k ) " { ( M + 1 ) } ) ) )
85 76 83 84 3syl 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) -> ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -onto-> ( 1 ... ( M + 1 ) ) )
88 foima 
 |-  ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -onto-> ( 1 ... ( M + 1 ) ) -> ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) = ( 1 ... ( M + 1 ) ) )
89 76 87 88 3syl 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( 2nd ` k ) : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) -> ( 2nd ` k ) Fn ( 1 ... ( M + 1 ) ) )
92 76 91 syl 
 |-  ( 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 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN )
94 3 93 syl 
 |-  ( ph -> ( M + 1 ) e. NN )
95 elfz1end 
 |-  ( ( M + 1 ) e. NN <-> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
96 94 95 sylib 
 |-  ( ph -> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
97 fnsnfv 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) -> { ( ( 2nd ` k ) ` ( M + 1 ) ) } = { ( M + 1 ) } )
100 98 99 sylan9req 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  1 e. ZZ
104 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
105 1m1e0 
 |-  ( 1 - 1 ) = 0
106 105 fveq2i 
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
107 104 106 eqtr4i 
 |-  NN0 = ( ZZ>= ` ( 1 - 1 ) )
108 3 107 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` ( 1 - 1 ) ) )
109 fzsuc2 
 |-  ( ( 1 e. ZZ /\ M e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
110 103 108 109 sylancr 
 |-  ( ph -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
111 110 difeq1d 
 |-  ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( ( ( 1 ... M ) u. { ( M + 1 ) } ) \ { ( M + 1 ) } ) )
112 difun2 
 |-  ( ( ( 1 ... M ) u. { ( M + 1 ) } ) \ { ( M + 1 ) } ) = ( ( 1 ... M ) \ { ( M + 1 ) } )
113 111 112 eqtrdi 
 |-  ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( ( 1 ... M ) \ { ( M + 1 ) } ) )
114 3 nn0red 
 |-  ( ph -> M e. RR )
115 ltp1 
 |-  ( M e. RR -> M < ( M + 1 ) )
116 peano2re 
 |-  ( M e. RR -> ( M + 1 ) e. RR )
117 ltnle 
 |-  ( ( M e. RR /\ ( M + 1 ) e. RR ) -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
118 116 117 mpdan 
 |-  ( M e. RR -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
119 115 118 mpbid 
 |-  ( M e. RR -> -. ( M + 1 ) <_ M )
120 114 119 syl 
 |-  ( ph -> -. ( M + 1 ) <_ M )
121 elfzle2 
 |-  ( ( M + 1 ) e. ( 1 ... M ) -> ( M + 1 ) <_ M )
122 120 121 nsyl 
 |-  ( ph -> -. ( M + 1 ) e. ( 1 ... M ) )
123 difsn 
 |-  ( -. ( M + 1 ) e. ( 1 ... M ) -> ( ( 1 ... M ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
124 122 123 syl 
 |-  ( ph -> ( ( 1 ... M ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
125 113 124 eqtrd 
 |-  ( ph -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
126 125 imaeq2d 
 |-  ( ph -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 2nd ` k ) " ( 1 ... M ) ) )
127 126 ad2antrr 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 129 f1oeq3d 
 |-  ( ( ( 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 ) ) )
131 81 130 mpbid 
 |-  ( ( ( 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 ) )
132 73 resex 
 |-  ( ( 2nd ` k ) |` ( 1 ... M ) ) e. _V
133 f1oeq1 
 |-  ( f = ( ( 2nd ` k ) |` ( 1 ... M ) ) -> ( f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( ( 2nd ` k ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
134 132 133 elab 
 |-  ( ( ( 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 ) )
135 131 134 sylibr 
 |-  ( ( ( 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 ) } )
136 71 135 opelxpd 
 |-  ( ( ( 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 ) } ) )
137 136 3ad2antr3 
 |-  ( ( ( 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 ) } ) )
138 3anass 
 |-  ( ( 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 ) ) ) )
139 138 biancomi 
 |-  ( ( 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 ) )
140 94 nnzd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
141 uzid 
 |-  ( ( M + 1 ) e. ZZ -> ( M + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
142 peano2uz 
 |-  ( ( M + 1 ) e. ( ZZ>= ` ( M + 1 ) ) -> ( ( M + 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
143 140 141 142 3syl 
 |-  ( ph -> ( ( M + 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
144 3 nn0zd 
 |-  ( ph -> M e. ZZ )
145 1 nnzd 
 |-  ( ph -> N e. ZZ )
146 zltp1le 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
147 peano2z 
 |-  ( M e. ZZ -> ( M + 1 ) e. ZZ )
148 eluz 
 |-  ( ( ( M + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( M + 1 ) <_ N ) )
149 147 148 sylan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( M + 1 ) <_ N ) )
150 146 149 bitr4d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
151 144 145 150 syl2anc 
 |-  ( ph -> ( M < N <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
152 4 151 mpbid 
 |-  ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
153 fzsplit2 
 |-  ( ( ( ( M + 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( M + 1 ) ... N ) = ( ( ( M + 1 ) ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
154 143 152 153 syl2anc 
 |-  ( ph -> ( ( M + 1 ) ... N ) = ( ( ( M + 1 ) ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
155 fzsn 
 |-  ( ( M + 1 ) e. ZZ -> ( ( M + 1 ) ... ( M + 1 ) ) = { ( M + 1 ) } )
156 140 155 syl 
 |-  ( ph -> ( ( M + 1 ) ... ( M + 1 ) ) = { ( M + 1 ) } )
157 156 uneq1d 
 |-  ( ph -> ( ( ( M + 1 ) ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) = ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
158 154 157 eqtrd 
 |-  ( ph -> ( ( M + 1 ) ... N ) = ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
159 158 xpeq1d 
 |-  ( ph -> ( ( ( M + 1 ) ... N ) X. { 0 } ) = ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
160 159 uneq2d 
 |-  ( 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 } ) ) )
161 xpundir 
 |-  ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) = ( ( { ( M + 1 ) } X. { 0 } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
162 ovex 
 |-  ( M + 1 ) e. _V
163 c0ex 
 |-  0 e. _V
164 162 163 xpsn 
 |-  ( { ( M + 1 ) } X. { 0 } ) = { <. ( M + 1 ) , 0 >. }
165 164 uneq1i 
 |-  ( ( { ( M + 1 ) } X. { 0 } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) = ( { <. ( M + 1 ) , 0 >. } u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
166 161 165 eqtri 
 |-  ( ( { ( M + 1 ) } u. ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) = ( { <. ( M + 1 ) , 0 >. } u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) )
167 166 uneq2i 
 |-  ( ( 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 } ) ) )
168 unass 
 |-  ( ( ( 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 } ) ) )
169 167 168 eqtr4i 
 |-  ( ( 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 } ) )
170 160 169 eqtrdi 
 |-  ( 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 } ) ) )
171 170 ad3antrrr 
 |-  ( ( ( ( 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 } ) ) )
172 162 a1i 
 |-  ( ( ( ( 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 )
173 163 a1i 
 |-  ( ( ( ( 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 )
174 110 eqcomd 
 |-  ( ph -> ( ( 1 ... M ) u. { ( M + 1 ) } ) = ( 1 ... ( M + 1 ) ) )
175 174 ad3antrrr 
 |-  ( ( ( ( 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 ) ) )
176 fveq2 
 |-  ( n = ( M + 1 ) -> ( ( 1st ` k ) ` n ) = ( ( 1st ` k ) ` ( M + 1 ) ) )
177 fveq2 
 |-  ( 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 ) ) )
178 176 177 oveq12d 
 |-  ( 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 + 1 ) ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) ) )
179 simplrl 
 |-  ( ( ( ( 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 ) ) -> ( ( 1st ` k ) ` ( M + 1 ) ) = 0 )
180 imain 
 |-  ( Fun `' ( 2nd ` k ) -> ( ( 2nd ` k ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... ( M + 1 ) ) ) ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) )
181 76 83 180 3syl 
 |-  ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( ( 2nd ` k ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... ( M + 1 ) ) ) ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) )
182 181 ad2antlr 
 |-  ( ( ( 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 ... j ) i^i ( ( j + 1 ) ... ( M + 1 ) ) ) ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) )
183 elfznn0 
 |-  ( j e. ( 0 ... M ) -> j e. NN0 )
184 183 nn0red 
 |-  ( j e. ( 0 ... M ) -> j e. RR )
185 184 ltp1d 
 |-  ( j e. ( 0 ... M ) -> j < ( j + 1 ) )
186 fzdisj 
 |-  ( j < ( j + 1 ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... ( M + 1 ) ) ) = (/) )
187 185 186 syl 
 |-  ( j e. ( 0 ... M ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... ( M + 1 ) ) ) = (/) )
188 187 imaeq2d 
 |-  ( j e. ( 0 ... M ) -> ( ( 2nd ` k ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... ( M + 1 ) ) ) ) = ( ( 2nd ` k ) " (/) ) )
189 ima0 
 |-  ( ( 2nd ` k ) " (/) ) = (/)
190 188 189 eqtrdi 
 |-  ( j e. ( 0 ... M ) -> ( ( 2nd ` k ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... ( M + 1 ) ) ) ) = (/) )
191 182 190 sylan9req 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) = (/) )
192 simplr 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) )
193 92 ad2antlr 
 |-  ( ( ( 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 ) Fn ( 1 ... ( M + 1 ) ) )
194 nn0p1nn 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN )
195 nnuz 
 |-  NN = ( ZZ>= ` 1 )
196 194 195 eleqtrdi 
 |-  ( j e. NN0 -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
197 fzss1 
 |-  ( ( j + 1 ) e. ( ZZ>= ` 1 ) -> ( ( j + 1 ) ... ( M + 1 ) ) C_ ( 1 ... ( M + 1 ) ) )
198 183 196 197 3syl 
 |-  ( j e. ( 0 ... M ) -> ( ( j + 1 ) ... ( M + 1 ) ) C_ ( 1 ... ( M + 1 ) ) )
199 elfzuz3 
 |-  ( j e. ( 0 ... M ) -> M e. ( ZZ>= ` j ) )
200 eluzp1p1 
 |-  ( M e. ( ZZ>= ` j ) -> ( M + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
201 eluzfz2 
 |-  ( ( M + 1 ) e. ( ZZ>= ` ( j + 1 ) ) -> ( M + 1 ) e. ( ( j + 1 ) ... ( M + 1 ) ) )
202 199 200 201 3syl 
 |-  ( j e. ( 0 ... M ) -> ( M + 1 ) e. ( ( j + 1 ) ... ( M + 1 ) ) )
203 198 202 jca 
 |-  ( j e. ( 0 ... M ) -> ( ( ( j + 1 ) ... ( M + 1 ) ) C_ ( 1 ... ( M + 1 ) ) /\ ( M + 1 ) e. ( ( j + 1 ) ... ( M + 1 ) ) ) )
204 fnfvima 
 |-  ( ( ( 2nd ` k ) Fn ( 1 ... ( M + 1 ) ) /\ ( ( j + 1 ) ... ( M + 1 ) ) C_ ( 1 ... ( M + 1 ) ) /\ ( M + 1 ) e. ( ( j + 1 ) ... ( M + 1 ) ) ) -> ( ( 2nd ` k ) ` ( M + 1 ) ) e. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
205 204 3expb 
 |-  ( ( ( 2nd ` k ) Fn ( 1 ... ( M + 1 ) ) /\ ( ( ( j + 1 ) ... ( M + 1 ) ) C_ ( 1 ... ( M + 1 ) ) /\ ( M + 1 ) e. ( ( j + 1 ) ... ( M + 1 ) ) ) ) -> ( ( 2nd ` k ) ` ( M + 1 ) ) e. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
206 193 203 205 syl2an 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( 2nd ` k ) ` ( M + 1 ) ) e. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
207 192 206 eqeltrrd 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( M + 1 ) e. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
208 1ex 
 |-  1 e. _V
209 fnconstg 
 |-  ( 1 e. _V -> ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) Fn ( ( 2nd ` k ) " ( 1 ... j ) ) )
210 208 209 ax-mp 
 |-  ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) Fn ( ( 2nd ` k ) " ( 1 ... j ) )
211 fnconstg 
 |-  ( 0 e. _V -> ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
212 163 211 ax-mp 
 |-  ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) )
213 fvun2 
 |-  ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) Fn ( ( 2nd ` k ) " ( 1 ... j ) ) /\ ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) /\ ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) = (/) /\ ( M + 1 ) e. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) = ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ` ( M + 1 ) ) )
214 210 212 213 mp3an12 
 |-  ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) = (/) /\ ( M + 1 ) e. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) = ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ` ( M + 1 ) ) )
215 191 207 214 syl2anc 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) = ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ` ( M + 1 ) ) )
216 163 fvconst2 
 |-  ( ( M + 1 ) e. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) -> ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ` ( M + 1 ) ) = 0 )
217 207 216 syl 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ` ( M + 1 ) ) = 0 )
218 215 217 eqtrd 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) = 0 )
219 218 adantlrl 
 |-  ( ( ( ( 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 ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) = 0 )
220 179 219 oveq12d 
 |-  ( ( ( ( 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 ) ) -> ( ( ( 1st ` k ) ` ( M + 1 ) ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) ) = ( 0 + 0 ) )
221 00id 
 |-  ( 0 + 0 ) = 0
222 220 221 eqtrdi 
 |-  ( ( ( ( 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 ) ) -> ( ( ( 1st ` k ) ` ( M + 1 ) ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` ( M + 1 ) ) ) = 0 )
223 178 222 sylan9eqr 
 |-  ( ( ( ( ( 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 = ( M + 1 ) ) -> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) = 0 )
224 172 173 175 223 fmptapd 
 |-  ( ( ( ( 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 ) , 0 >. } ) = ( n e. ( 1 ... ( M + 1 ) ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) )
225 224 uneq1d 
 |-  ( ( ( ( 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 ) , 0 >. } ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) = ( ( n e. ( 1 ... ( M + 1 ) ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
226 171 225 eqtrd 
 |-  ( ( ( ( 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 + 1 ) ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
227 elmapfn 
 |-  ( ( 1st ` k ) e. ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) -> ( 1st ` k ) Fn ( 1 ... ( M + 1 ) ) )
228 61 227 syl 
 |-  ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( 1st ` k ) Fn ( 1 ... ( M + 1 ) ) )
229 fnssres 
 |-  ( ( ( 1st ` k ) Fn ( 1 ... ( M + 1 ) ) /\ ( 1 ... M ) C_ ( 1 ... ( M + 1 ) ) ) -> ( ( 1st ` k ) |` ( 1 ... M ) ) Fn ( 1 ... M ) )
230 228 64 229 sylancl 
 |-  ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( ( 1st ` k ) |` ( 1 ... M ) ) Fn ( 1 ... M ) )
231 230 ad3antlr 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( 1st ` k ) |` ( 1 ... M ) ) Fn ( 1 ... M ) )
232 fnconstg 
 |-  ( 0 e. _V -> ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) )
233 163 232 ax-mp 
 |-  ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) )
234 210 233 pm3.2i 
 |-  ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) Fn ( ( 2nd ` k ) " ( 1 ... j ) ) /\ ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) )
235 imain 
 |-  ( Fun `' ( 2nd ` k ) -> ( ( 2nd ` k ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... M ) ) ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) )
236 76 83 235 3syl 
 |-  ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> ( ( 2nd ` k ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... M ) ) ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) )
237 fzdisj 
 |-  ( j < ( j + 1 ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... M ) ) = (/) )
238 185 237 syl 
 |-  ( j e. ( 0 ... M ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... M ) ) = (/) )
239 238 imaeq2d 
 |-  ( j e. ( 0 ... M ) -> ( ( 2nd ` k ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... M ) ) ) = ( ( 2nd ` k ) " (/) ) )
240 239 189 eqtrdi 
 |-  ( j e. ( 0 ... M ) -> ( ( 2nd ` k ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... M ) ) ) = (/) )
241 236 240 sylan9req 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) = (/) )
242 fnun 
 |-  ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) Fn ( ( 2nd ` k ) " ( 1 ... j ) ) /\ ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) /\ ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) = (/) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) )
243 234 241 242 sylancr 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) )
244 243 ad4ant24 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) )
245 101 adantr 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) \ ( ( 2nd ` k ) " { ( M + 1 ) } ) ) = ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) )
246 85 ad3antlr 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) \ ( ( 2nd ` k ) " { ( M + 1 ) } ) ) )
247 183 194 syl 
 |-  ( j e. ( 0 ... M ) -> ( j + 1 ) e. NN )
248 247 195 eleqtrdi 
 |-  ( j e. ( 0 ... M ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
249 fzsplit2 
 |-  ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ M e. ( ZZ>= ` j ) ) -> ( 1 ... M ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... M ) ) )
250 248 199 249 syl2anc 
 |-  ( j e. ( 0 ... M ) -> ( 1 ... M ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... M ) ) )
251 128 250 sylan9eq 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... M ) ) )
252 251 imaeq2d 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( 2nd ` k ) " ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 2nd ` k ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... M ) ) ) )
253 246 252 eqtr3d 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) \ ( ( 2nd ` k ) " { ( M + 1 ) } ) ) = ( ( 2nd ` k ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... M ) ) ) )
254 125 ad3antrrr 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) = ( 1 ... M ) )
255 245 253 254 3eqtr3rd 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( 1 ... M ) = ( ( 2nd ` k ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... M ) ) ) )
256 imaundi 
 |-  ( ( 2nd ` k ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... M ) ) ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) )
257 255 256 eqtrdi 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( 1 ... M ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) )
258 257 fneq2d 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) <-> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) ) ) )
259 244 258 mpbird 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) )
260 fzss2 
 |-  ( M e. ( ZZ>= ` j ) -> ( 1 ... j ) C_ ( 1 ... M ) )
261 resima2 
 |-  ( ( 1 ... j ) C_ ( 1 ... M ) -> ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) = ( ( 2nd ` k ) " ( 1 ... j ) ) )
262 199 260 261 3syl 
 |-  ( j e. ( 0 ... M ) -> ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) = ( ( 2nd ` k ) " ( 1 ... j ) ) )
263 262 xpeq1d 
 |-  ( j e. ( 0 ... M ) -> ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) )
264 183 196 syl 
 |-  ( j e. ( 0 ... M ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
265 fzss1 
 |-  ( ( j + 1 ) e. ( ZZ>= ` 1 ) -> ( ( j + 1 ) ... M ) C_ ( 1 ... M ) )
266 resima2 
 |-  ( ( ( j + 1 ) ... M ) C_ ( 1 ... M ) -> ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) = ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) )
267 264 265 266 3syl 
 |-  ( j e. ( 0 ... M ) -> ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) = ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) )
268 267 xpeq1d 
 |-  ( j e. ( 0 ... M ) -> ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) = ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) )
269 263 268 uneq12d 
 |-  ( j e. ( 0 ... M ) -> ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) )
270 269 adantl 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) )
271 270 fneq1d 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) <-> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) ) )
272 259 271 mpbird 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) )
273 fzfid 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( 1 ... M ) e. Fin )
274 inidm 
 |-  ( ( 1 ... M ) i^i ( 1 ... M ) ) = ( 1 ... M )
275 fvres 
 |-  ( n e. ( 1 ... M ) -> ( ( ( 1st ` k ) |` ( 1 ... M ) ) ` n ) = ( ( 1st ` k ) ` n ) )
276 275 adantl 
 |-  ( ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) /\ n e. ( 1 ... M ) ) -> ( ( ( 1st ` k ) |` ( 1 ... M ) ) ` n ) = ( ( 1st ` k ) ` n ) )
277 disjsn 
 |-  ( ( ( 1 ... M ) i^i { ( M + 1 ) } ) = (/) <-> -. ( M + 1 ) e. ( 1 ... M ) )
278 122 277 sylibr 
 |-  ( ph -> ( ( 1 ... M ) i^i { ( M + 1 ) } ) = (/) )
279 278 ad3antrrr 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( 1 ... M ) i^i { ( M + 1 ) } ) = (/) )
280 259 279 jca 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) /\ ( ( 1 ... M ) i^i { ( M + 1 ) } ) = (/) ) )
281 fnconstg 
 |-  ( 0 e. _V -> ( { ( M + 1 ) } X. { 0 } ) Fn { ( M + 1 ) } )
282 163 281 ax-mp 
 |-  ( { ( M + 1 ) } X. { 0 } ) Fn { ( M + 1 ) }
283 fvun1 
 |-  ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) /\ ( { ( M + 1 ) } X. { 0 } ) Fn { ( M + 1 ) } /\ ( ( ( 1 ... M ) i^i { ( M + 1 ) } ) = (/) /\ n e. ( 1 ... M ) ) ) -> ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) )
284 282 283 mp3an2 
 |-  ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) /\ ( ( ( 1 ... M ) i^i { ( M + 1 ) } ) = (/) /\ n e. ( 1 ... M ) ) ) -> ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) )
285 284 anassrs 
 |-  ( ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) Fn ( 1 ... M ) /\ ( ( 1 ... M ) i^i { ( M + 1 ) } ) = (/) ) /\ n e. ( 1 ... M ) ) -> ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) )
286 280 285 sylan 
 |-  ( ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) /\ n e. ( 1 ... M ) ) -> ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) )
287 247 nnzd 
 |-  ( j e. ( 0 ... M ) -> ( j + 1 ) e. ZZ )
288 183 nn0cnd 
 |-  ( j e. ( 0 ... M ) -> j e. CC )
289 pncan1 
 |-  ( j e. CC -> ( ( j + 1 ) - 1 ) = j )
290 288 289 syl 
 |-  ( j e. ( 0 ... M ) -> ( ( j + 1 ) - 1 ) = j )
291 290 fveq2d 
 |-  ( j e. ( 0 ... M ) -> ( ZZ>= ` ( ( j + 1 ) - 1 ) ) = ( ZZ>= ` j ) )
292 199 291 eleqtrrd 
 |-  ( j e. ( 0 ... M ) -> M e. ( ZZ>= ` ( ( j + 1 ) - 1 ) ) )
293 fzsuc2 
 |-  ( ( ( j + 1 ) e. ZZ /\ M e. ( ZZ>= ` ( ( j + 1 ) - 1 ) ) ) -> ( ( j + 1 ) ... ( M + 1 ) ) = ( ( ( j + 1 ) ... M ) u. { ( M + 1 ) } ) )
294 287 292 293 syl2anc 
 |-  ( j e. ( 0 ... M ) -> ( ( j + 1 ) ... ( M + 1 ) ) = ( ( ( j + 1 ) ... M ) u. { ( M + 1 ) } ) )
295 294 imaeq2d 
 |-  ( j e. ( 0 ... M ) -> ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) = ( ( 2nd ` k ) " ( ( ( j + 1 ) ... M ) u. { ( M + 1 ) } ) ) )
296 imaundi 
 |-  ( ( 2nd ` k ) " ( ( ( j + 1 ) ... M ) u. { ( M + 1 ) } ) ) = ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) u. ( ( 2nd ` k ) " { ( M + 1 ) } ) )
297 295 296 eqtrdi 
 |-  ( j e. ( 0 ... M ) -> ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) = ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) u. ( ( 2nd ` k ) " { ( M + 1 ) } ) ) )
298 297 xpeq1d 
 |-  ( j e. ( 0 ... M ) -> ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) = ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) u. ( ( 2nd ` k ) " { ( M + 1 ) } ) ) X. { 0 } ) )
299 xpundir 
 |-  ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) u. ( ( 2nd ` k ) " { ( M + 1 ) } ) ) X. { 0 } ) = ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) )
300 298 299 eqtrdi 
 |-  ( j e. ( 0 ... M ) -> ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) = ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) ) )
301 300 uneq2d 
 |-  ( j e. ( 0 ... M ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) ) ) )
302 unass 
 |-  ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) ) = ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) ) )
303 301 302 eqtr4di 
 |-  ( j e. ( 0 ... M ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) ) )
304 303 adantl 
 |-  ( ( ( ph /\ k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) ) )
305 98 xpeq1d 
 |-  ( ( 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 ) ) } X. { 0 } ) = ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) )
306 305 uneq2d 
 |-  ( ( ph /\ k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` k ) ` ( M + 1 ) ) } X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) ) )
307 306 adantr 
 |-  ( ( ( ph /\ k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` k ) ` ( M + 1 ) ) } X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( ( ( 2nd ` k ) " { ( M + 1 ) } ) X. { 0 } ) ) )
308 304 307 eqtr4d 
 |-  ( ( ( ph /\ k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` k ) ` ( M + 1 ) ) } X. { 0 } ) ) )
309 99 xpeq1d 
 |-  ( ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) -> ( { ( ( 2nd ` k ) ` ( M + 1 ) ) } X. { 0 } ) = ( { ( M + 1 ) } X. { 0 } ) )
310 309 uneq2d 
 |-  ( ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` k ) ` ( M + 1 ) ) } X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) )
311 308 310 sylan9eq 
 |-  ( ( ( ( ph /\ k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) /\ j e. ( 0 ... M ) ) /\ ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) )
312 311 an32s 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) )
313 312 fveq1d 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 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 ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) ` n ) )
314 313 adantr 
 |-  ( ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) /\ n e. ( 1 ... M ) ) -> ( ( ( ( ( 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 ) ) X. { 0 } ) ) u. ( { ( M + 1 ) } X. { 0 } ) ) ` n ) )
315 269 fveq1d 
 |-  ( j e. ( 0 ... M ) -> ( ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) )
316 315 ad2antlr 
 |-  ( ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) /\ n e. ( 1 ... M ) ) -> ( ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) )
317 286 314 316 3eqtr4rd 
 |-  ( ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) /\ n e. ( 1 ... M ) ) -> ( ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) )
318 231 272 273 273 274 276 317 offval 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) 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 ) ) ) )
319 318 uneq1d 
 |-  ( ( ( ( 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 ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) 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 ) ... N ) X. { 0 } ) ) )
320 319 adantlrl 
 |-  ( ( ( ( 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 ) ) -> ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) 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 ) ... N ) X. { 0 } ) ) )
321 228 adantr 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( 1st ` k ) Fn ( 1 ... ( M + 1 ) ) )
322 210 212 pm3.2i 
 |-  ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) Fn ( ( 2nd ` k ) " ( 1 ... j ) ) /\ ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
323 181 190 sylan9req 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) = (/) )
324 fnun 
 |-  ( ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) Fn ( ( 2nd ` k ) " ( 1 ... j ) ) /\ ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) Fn ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) /\ ( ( ( 2nd ` k ) " ( 1 ... j ) ) i^i ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) = (/) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) )
325 322 323 324 sylancr 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) )
326 peano2uz 
 |-  ( M e. ( ZZ>= ` j ) -> ( M + 1 ) e. ( ZZ>= ` j ) )
327 199 326 syl 
 |-  ( j e. ( 0 ... M ) -> ( M + 1 ) e. ( ZZ>= ` j ) )
328 fzsplit2 
 |-  ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ ( M + 1 ) e. ( ZZ>= ` j ) ) -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... ( M + 1 ) ) ) )
329 264 327 328 syl2anc 
 |-  ( j e. ( 0 ... M ) -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... ( M + 1 ) ) ) )
330 329 imaeq2d 
 |-  ( j e. ( 0 ... M ) -> ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) = ( ( 2nd ` k ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... ( M + 1 ) ) ) ) )
331 imaundi 
 |-  ( ( 2nd ` k ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... ( M + 1 ) ) ) ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
332 330 331 eqtr2di 
 |-  ( j e. ( 0 ... M ) -> ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) = ( ( 2nd ` k ) " ( 1 ... ( M + 1 ) ) ) )
333 332 89 sylan9eqr 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) = ( 1 ... ( M + 1 ) ) )
334 333 fneq2d 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` k ) " ( 1 ... j ) ) u. ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) ) <-> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) Fn ( 1 ... ( M + 1 ) ) ) )
335 325 334 mpbid 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) Fn ( 1 ... ( M + 1 ) ) )
336 fzfid 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( 1 ... ( M + 1 ) ) e. Fin )
337 inidm 
 |-  ( ( 1 ... ( M + 1 ) ) i^i ( 1 ... ( M + 1 ) ) ) = ( 1 ... ( M + 1 ) )
338 eqidd 
 |-  ( ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) /\ n e. ( 1 ... ( M + 1 ) ) ) -> ( ( 1st ` k ) ` n ) = ( ( 1st ` k ) ` n ) )
339 eqidd 
 |-  ( ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) /\ n e. ( 1 ... ( 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 } ) ) ` n ) )
340 321 335 336 336 337 338 339 offval 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) = ( n e. ( 1 ... ( M + 1 ) ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) )
341 340 uneq1d 
 |-  ( ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ j e. ( 0 ... M ) ) -> ( ( ( 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 } ) ) = ( ( n e. ( 1 ... ( M + 1 ) ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
342 341 ad4ant24 
 |-  ( ( ( ( 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 ) ) -> ( ( ( 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 } ) ) = ( ( n e. ( 1 ... ( M + 1 ) ) |-> ( ( ( 1st ` k ) ` n ) + ( ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ` n ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
343 226 320 342 3eqtr4rd 
 |-  ( ( ( ( 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 ) ) -> ( ( ( 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 } ) ) = ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) )
344 343 csbeq1d 
 |-  ( ( ( ( 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 ) ) -> [_ ( ( ( 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 ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
345 344 eqeq2d 
 |-  ( ( ( ( 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 ) ) -> ( 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 <-> i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
346 345 rexbidva 
 |-  ( ( ( 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 ) ) ) -> ( 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 <-> E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
347 346 ralbidv 
 |-  ( ( ( 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 ) ) ) -> ( 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 <-> A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
348 347 biimpd 
 |-  ( ( ( 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 ) ) ) -> ( 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 -> A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
349 348 impr 
 |-  ( ( ( 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 ) ) /\ 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 ) ) -> A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
350 139 349 sylan2b 
 |-  ( ( ( 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 ) ) ) -> A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
351 1st2nd2 
 |-  ( k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) -> k = <. ( 1st ` k ) , ( 2nd ` k ) >. )
352 351 ad2antlr 
 |-  ( ( ( 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 ) ) ) -> k = <. ( 1st ` k ) , ( 2nd ` k ) >. )
353 fnsnsplit 
 |-  ( ( ( 1st ` k ) Fn ( 1 ... ( M + 1 ) ) /\ ( M + 1 ) e. ( 1 ... ( M + 1 ) ) ) -> ( 1st ` k ) = ( ( ( 1st ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 1st ` k ) ` ( M + 1 ) ) >. } ) )
354 228 96 353 syl2anr 
 |-  ( ( ph /\ k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) -> ( 1st ` k ) = ( ( ( 1st ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 1st ` k ) ` ( M + 1 ) ) >. } ) )
355 354 adantr 
 |-  ( ( ( 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 ) -> ( 1st ` k ) = ( ( ( 1st ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 1st ` k ) ` ( M + 1 ) ) >. } ) )
356 125 reseq2d 
 |-  ( ph -> ( ( 1st ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 1st ` k ) |` ( 1 ... M ) ) )
357 356 adantr 
 |-  ( ( ph /\ 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 + 1 ) } ) ) = ( ( 1st ` k ) |` ( 1 ... M ) ) )
358 opeq2 
 |-  ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 -> <. ( M + 1 ) , ( ( 1st ` k ) ` ( M + 1 ) ) >. = <. ( M + 1 ) , 0 >. )
359 358 sneqd 
 |-  ( ( ( 1st ` k ) ` ( M + 1 ) ) = 0 -> { <. ( M + 1 ) , ( ( 1st ` k ) ` ( M + 1 ) ) >. } = { <. ( M + 1 ) , 0 >. } )
360 uneq12 
 |-  ( ( ( ( 1st ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 1st ` k ) |` ( 1 ... M ) ) /\ { <. ( M + 1 ) , ( ( 1st ` k ) ` ( M + 1 ) ) >. } = { <. ( M + 1 ) , 0 >. } ) -> ( ( ( 1st ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 1st ` k ) ` ( M + 1 ) ) >. } ) = ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) )
361 357 359 360 syl2an 
 |-  ( ( ( 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 ) -> ( ( ( 1st ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 1st ` k ) ` ( M + 1 ) ) >. } ) = ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) )
362 355 361 eqtrd 
 |-  ( ( ( 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 ) -> ( 1st ` k ) = ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) )
363 362 adantrr 
 |-  ( ( ( 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 ) ) ) -> ( 1st ` k ) = ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) )
364 fnsnsplit 
 |-  ( ( ( 2nd ` k ) Fn ( 1 ... ( M + 1 ) ) /\ ( M + 1 ) e. ( 1 ... ( M + 1 ) ) ) -> ( 2nd ` k ) = ( ( ( 2nd ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 2nd ` k ) ` ( M + 1 ) ) >. } ) )
365 92 96 364 syl2anr 
 |-  ( ( ph /\ k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) -> ( 2nd ` k ) = ( ( ( 2nd ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 2nd ` k ) ` ( M + 1 ) ) >. } ) )
366 365 adantr 
 |-  ( ( ( 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 ) = ( ( ( 2nd ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 2nd ` k ) ` ( M + 1 ) ) >. } ) )
367 125 reseq2d 
 |-  ( ph -> ( ( 2nd ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 2nd ` k ) |` ( 1 ... M ) ) )
368 367 adantr 
 |-  ( ( ph /\ 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 ) ) )
369 opeq2 
 |-  ( ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) -> <. ( M + 1 ) , ( ( 2nd ` k ) ` ( M + 1 ) ) >. = <. ( M + 1 ) , ( M + 1 ) >. )
370 369 sneqd 
 |-  ( ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) -> { <. ( M + 1 ) , ( ( 2nd ` k ) ` ( M + 1 ) ) >. } = { <. ( M + 1 ) , ( M + 1 ) >. } )
371 uneq12 
 |-  ( ( ( ( 2nd ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) = ( ( 2nd ` k ) |` ( 1 ... M ) ) /\ { <. ( M + 1 ) , ( ( 2nd ` k ) ` ( M + 1 ) ) >. } = { <. ( M + 1 ) , ( M + 1 ) >. } ) -> ( ( ( 2nd ` k ) |` ( ( 1 ... ( M + 1 ) ) \ { ( M + 1 ) } ) ) u. { <. ( M + 1 ) , ( ( 2nd ` k ) ` ( M + 1 ) ) >. } ) = ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) )
372 368 370 371 syl2an 
 |-  ( ( ( 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 ) } ) ) u. { <. ( M + 1 ) , ( ( 2nd ` k ) ` ( M + 1 ) ) >. } ) = ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) )
373 366 372 eqtrd 
 |-  ( ( ( 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 ) = ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) )
374 373 adantrl 
 |-  ( ( ( 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 ) ) ) -> ( 2nd ` k ) = ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) )
375 363 374 opeq12d 
 |-  ( ( ( 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 ) ) ) -> <. ( 1st ` k ) , ( 2nd ` k ) >. = <. ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. )
376 352 375 eqtrd 
 |-  ( ( ( 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 ) ) ) -> k = <. ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. )
377 376 3adantr1 
 |-  ( ( ( 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 ) ) ) -> k = <. ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. )
378 fvex 
 |-  ( 1st ` k ) e. _V
379 378 resex 
 |-  ( ( 1st ` k ) |` ( 1 ... M ) ) e. _V
380 379 132 op1std 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( 1st ` t ) = ( ( 1st ` k ) |` ( 1 ... M ) ) )
381 379 132 op2ndd 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( 2nd ` t ) = ( ( 2nd ` k ) |` ( 1 ... M ) ) )
382 381 imaeq1d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( 2nd ` t ) " ( 1 ... j ) ) = ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) )
383 382 xpeq1d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) )
384 381 imaeq1d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) = ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) )
385 384 xpeq1d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) = ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) )
386 383 385 uneq12d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) )
387 380 386 oveq12d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) = ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) )
388 387 uneq1d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) = ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) )
389 388 csbeq1d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> [_ ( ( ( 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 ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
390 389 eqeq2d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... 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 <-> i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
391 390 rexbidv 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... 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 <-> E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
392 391 ralbidv 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 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 <-> A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( ( 1st ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
393 380 uneq1d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) = ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) )
394 381 uneq1d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) )
395 393 394 opeq12d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. = <. ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. )
396 395 eqeq2d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. -> ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. <-> k = <. ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
397 392 396 anbi12d 
 |-  ( t = <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 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 /\ k = <. ( ( 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 ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ k = <. ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) ) )
398 397 rspcev 
 |-  ( ( <. ( ( 1st ` k ) |` ( 1 ... M ) ) , ( ( 2nd ` k ) |` ( 1 ... M ) ) >. 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 ` k ) |` ( 1 ... M ) ) oF + ( ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` k ) |` ( 1 ... M ) ) " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ k = <. ( ( ( 1st ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( ( 2nd ` k ) |` ( 1 ... M ) ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) ) -> E. 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 /\ k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
399 137 350 377 398 syl12anc 
 |-  ( ( ( 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 ) ) ) -> E. 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 /\ k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
400 399 ex 
 |-  ( ( 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 ) ) -> E. 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 /\ k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) ) )
401 elrabi 
 |-  ( 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 } -> t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )
402 elrabi 
 |-  ( n 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 } -> n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )
403 401 402 anim12i 
 |-  ( ( 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 } /\ n 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 } ) -> ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) )
404 eqtr2 
 |-  ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. )
405 22 24 opth 
 |-  ( <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. <-> ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) /\ ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) ) )
406 difeq1 
 |-  ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) -> ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) \ { <. ( M + 1 ) , 0 >. } ) )
407 difun2 
 |-  ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } )
408 difun2 
 |-  ( ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } )
409 406 407 408 3eqtr3g 
 |-  ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) -> ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) )
410 difeq1 
 |-  ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) -> ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) )
411 difun2 
 |-  ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } )
412 difun2 
 |-  ( ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } )
413 410 411 412 3eqtr3g 
 |-  ( ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) -> ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) )
414 409 413 anim12i 
 |-  ( ( ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) /\ ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) ) -> ( ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) /\ ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) ) )
415 405 414 sylbi 
 |-  ( <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. -> ( ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) /\ ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) ) )
416 404 415 syl 
 |-  ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> ( ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) /\ ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) ) )
417 elmapfn 
 |-  ( ( 1st ` t ) e. ( ( 0 ..^ K ) ^m ( 1 ... M ) ) -> ( 1st ` t ) Fn ( 1 ... M ) )
418 fnop 
 |-  ( ( ( 1st ` t ) Fn ( 1 ... M ) /\ <. ( M + 1 ) , 0 >. e. ( 1st ` t ) ) -> ( M + 1 ) e. ( 1 ... M ) )
419 418 ex 
 |-  ( ( 1st ` t ) Fn ( 1 ... M ) -> ( <. ( M + 1 ) , 0 >. e. ( 1st ` t ) -> ( M + 1 ) e. ( 1 ... M ) ) )
420 9 417 419 3syl 
 |-  ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( <. ( M + 1 ) , 0 >. e. ( 1st ` t ) -> ( M + 1 ) e. ( 1 ... M ) ) )
421 420 122 nsyli 
 |-  ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( ph -> -. <. ( M + 1 ) , 0 >. e. ( 1st ` t ) ) )
422 421 impcom 
 |-  ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> -. <. ( M + 1 ) , 0 >. e. ( 1st ` t ) )
423 difsn 
 |-  ( -. <. ( M + 1 ) , 0 >. e. ( 1st ` t ) -> ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( 1st ` t ) )
424 422 423 syl 
 |-  ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( 1st ` t ) )
425 xp1st 
 |-  ( n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( 1st ` n ) e. ( ( 0 ..^ K ) ^m ( 1 ... M ) ) )
426 elmapfn 
 |-  ( ( 1st ` n ) e. ( ( 0 ..^ K ) ^m ( 1 ... M ) ) -> ( 1st ` n ) Fn ( 1 ... M ) )
427 fnop 
 |-  ( ( ( 1st ` n ) Fn ( 1 ... M ) /\ <. ( M + 1 ) , 0 >. e. ( 1st ` n ) ) -> ( M + 1 ) e. ( 1 ... M ) )
428 427 ex 
 |-  ( ( 1st ` n ) Fn ( 1 ... M ) -> ( <. ( M + 1 ) , 0 >. e. ( 1st ` n ) -> ( M + 1 ) e. ( 1 ... M ) ) )
429 425 426 428 3syl 
 |-  ( n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( <. ( M + 1 ) , 0 >. e. ( 1st ` n ) -> ( M + 1 ) e. ( 1 ... M ) ) )
430 429 122 nsyli 
 |-  ( n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( ph -> -. <. ( M + 1 ) , 0 >. e. ( 1st ` n ) ) )
431 430 impcom 
 |-  ( ( ph /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> -. <. ( M + 1 ) , 0 >. e. ( 1st ` n ) )
432 difsn 
 |-  ( -. <. ( M + 1 ) , 0 >. e. ( 1st ` n ) -> ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) = ( 1st ` n ) )
433 431 432 syl 
 |-  ( ( ph /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) = ( 1st ` n ) )
434 424 433 eqeqan12d 
 |-  ( ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) /\ ( ph /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) ) -> ( ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) <-> ( 1st ` t ) = ( 1st ` n ) ) )
435 434 anandis 
 |-  ( ( ph /\ ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) ) -> ( ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) <-> ( 1st ` t ) = ( 1st ` n ) ) )
436 f1ofn 
 |-  ( ( 2nd ` t ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) -> ( 2nd ` t ) Fn ( 1 ... M ) )
437 fnop 
 |-  ( ( ( 2nd ` t ) Fn ( 1 ... M ) /\ <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` t ) ) -> ( M + 1 ) e. ( 1 ... M ) )
438 437 ex 
 |-  ( ( 2nd ` t ) Fn ( 1 ... M ) -> ( <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` t ) -> ( M + 1 ) e. ( 1 ... M ) ) )
439 17 436 438 3syl 
 |-  ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` t ) -> ( M + 1 ) e. ( 1 ... M ) ) )
440 439 122 nsyli 
 |-  ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( ph -> -. <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` t ) ) )
441 440 impcom 
 |-  ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> -. <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` t ) )
442 difsn 
 |-  ( -. <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` t ) -> ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( 2nd ` t ) )
443 441 442 syl 
 |-  ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( 2nd ` t ) )
444 xp2nd 
 |-  ( n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( 2nd ` n ) e. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } )
445 fvex 
 |-  ( 2nd ` n ) e. _V
446 f1oeq1 
 |-  ( f = ( 2nd ` n ) -> ( f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( 2nd ` n ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
447 445 446 elab 
 |-  ( ( 2nd ` n ) e. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } <-> ( 2nd ` n ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
448 444 447 sylib 
 |-  ( n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( 2nd ` n ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
449 f1ofn 
 |-  ( ( 2nd ` n ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) -> ( 2nd ` n ) Fn ( 1 ... M ) )
450 fnop 
 |-  ( ( ( 2nd ` n ) Fn ( 1 ... M ) /\ <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` n ) ) -> ( M + 1 ) e. ( 1 ... M ) )
451 450 ex 
 |-  ( ( 2nd ` n ) Fn ( 1 ... M ) -> ( <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` n ) -> ( M + 1 ) e. ( 1 ... M ) ) )
452 448 449 451 3syl 
 |-  ( n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` n ) -> ( M + 1 ) e. ( 1 ... M ) ) )
453 452 122 nsyli 
 |-  ( n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) -> ( ph -> -. <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` n ) ) )
454 453 impcom 
 |-  ( ( ph /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> -. <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` n ) )
455 difsn 
 |-  ( -. <. ( M + 1 ) , ( M + 1 ) >. e. ( 2nd ` n ) -> ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( 2nd ` n ) )
456 454 455 syl 
 |-  ( ( ph /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( 2nd ` n ) )
457 443 456 eqeqan12d 
 |-  ( ( ( ph /\ t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) /\ ( ph /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) ) -> ( ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) <-> ( 2nd ` t ) = ( 2nd ` n ) ) )
458 457 anandis 
 |-  ( ( ph /\ ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) ) -> ( ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) <-> ( 2nd ` t ) = ( 2nd ` n ) ) )
459 435 458 anbi12d 
 |-  ( ( ph /\ ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) ) -> ( ( ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) /\ ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) ) <-> ( ( 1st ` t ) = ( 1st ` n ) /\ ( 2nd ` t ) = ( 2nd ` n ) ) ) )
460 xpopth 
 |-  ( ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) -> ( ( ( 1st ` t ) = ( 1st ` n ) /\ ( 2nd ` t ) = ( 2nd ` n ) ) <-> t = n ) )
461 460 adantl 
 |-  ( ( ph /\ ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) ) -> ( ( ( 1st ` t ) = ( 1st ` n ) /\ ( 2nd ` t ) = ( 2nd ` n ) ) <-> t = n ) )
462 459 461 bitrd 
 |-  ( ( ph /\ ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) ) -> ( ( ( ( 1st ` t ) \ { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) \ { <. ( M + 1 ) , 0 >. } ) /\ ( ( 2nd ` t ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) \ { <. ( M + 1 ) , ( M + 1 ) >. } ) ) <-> t = n ) )
463 416 462 imbitrid 
 |-  ( ( ph /\ ( t e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) /\ n e. ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ) ) -> ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) )
464 403 463 sylan2 
 |-  ( ( ph /\ ( 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 } /\ n 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 } ) ) -> ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) )
465 464 ralrimivva 
 |-  ( 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 } A. n 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 } ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) )
466 465 adantr 
 |-  ( ( ph /\ k e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) ) -> 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 } A. n 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 } ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) )
467 400 466 jctird 
 |-  ( ( 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 ) ) -> ( E. 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 /\ k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) /\ 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 } A. n 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 } ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) ) ) )
468 fveq2 
 |-  ( t = n -> ( 1st ` t ) = ( 1st ` n ) )
469 468 uneq1d 
 |-  ( t = n -> ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) = ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) )
470 fveq2 
 |-  ( t = n -> ( 2nd ` t ) = ( 2nd ` n ) )
471 470 uneq1d 
 |-  ( t = n -> ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) = ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) )
472 469 471 opeq12d 
 |-  ( t = n -> <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. )
473 472 eqeq2d 
 |-  ( t = n -> ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. <-> k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
474 473 reu4 
 |-  ( E! 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. <-> ( E. 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ 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 } A. n 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 } ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) ) )
475 58 rexrab 
 |-  ( E. 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. <-> E. 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 /\ k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
476 475 anbi1i 
 |-  ( ( E. 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ 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 } A. n 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 } ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) ) <-> ( E. 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 /\ k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) /\ 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 } A. n 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 } ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) ) )
477 474 476 bitri 
 |-  ( E! 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. <-> ( E. 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 /\ k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) /\ 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 } A. n 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 } ( ( k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. /\ k = <. ( ( 1st ` n ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` n ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) -> t = n ) ) )
478 467 477 imbitrrdi 
 |-  ( ( 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 ) ) -> E! 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
479 478 ralrimiva 
 |-  ( ph -> A. 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 ) ) -> E! 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
480 fveq2 
 |-  ( s = k -> ( 1st ` s ) = ( 1st ` k ) )
481 fveq2 
 |-  ( s = k -> ( 2nd ` s ) = ( 2nd ` k ) )
482 481 imaeq1d 
 |-  ( s = k -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` k ) " ( 1 ... j ) ) )
483 482 xpeq1d 
 |-  ( s = k -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) )
484 481 imaeq1d 
 |-  ( s = k -> ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) = ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) )
485 484 xpeq1d 
 |-  ( s = k -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) = ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) )
486 483 485 uneq12d 
 |-  ( s = k -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) )
487 480 486 oveq12d 
 |-  ( s = k -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) = ( ( 1st ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) )
488 487 uneq1d 
 |-  ( s = k -> ( ( ( 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 ` k ) oF + ( ( ( ( 2nd ` k ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` k ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
489 488 csbeq1d 
 |-  ( s = k -> [_ ( ( ( 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 ` 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 )
490 489 eqeq2d 
 |-  ( s = k -> ( 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 ` 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 ) )
491 490 rexbidv 
 |-  ( s = k -> ( 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 ` 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 ) )
492 491 ralbidv 
 |-  ( s = k -> ( 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 ` 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 ) )
493 480 fveq1d 
 |-  ( s = k -> ( ( 1st ` s ) ` ( M + 1 ) ) = ( ( 1st ` k ) ` ( M + 1 ) ) )
494 493 eqeq1d 
 |-  ( s = k -> ( ( ( 1st ` s ) ` ( M + 1 ) ) = 0 <-> ( ( 1st ` k ) ` ( M + 1 ) ) = 0 ) )
495 481 fveq1d 
 |-  ( s = k -> ( ( 2nd ` s ) ` ( M + 1 ) ) = ( ( 2nd ` k ) ` ( M + 1 ) ) )
496 495 eqeq1d 
 |-  ( s = k -> ( ( ( 2nd ` s ) ` ( M + 1 ) ) = ( M + 1 ) <-> ( ( 2nd ` k ) ` ( M + 1 ) ) = ( M + 1 ) ) )
497 492 494 496 3anbi123d 
 |-  ( s = k -> ( ( 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 ` 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 ) ) ) )
498 497 ralrab 
 |-  ( A. k 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 ) ) } E! 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. <-> A. 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 ) ) -> E! 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
499 479 498 sylibr 
 |-  ( ph -> A. k 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 ) ) } E! 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. )
500 eqid 
 |-  ( 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 ) >. } ) >. ) = ( 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 ) >. } ) >. )
501 500 f1ompt 
 |-  ( ( 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 ) >. } ) >. ) : { 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 } -1-1-onto-> { 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. { 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. k 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 ) ) } E! 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 } k = <. ( ( 1st ` t ) u. { <. ( M + 1 ) , 0 >. } ) , ( ( 2nd ` t ) u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. ) )
502 60 499 501 sylanbrc 
 |-  ( ph -> ( 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 ) >. } ) >. ) : { 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 } -1-1-onto-> { 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 ) ) } )
503 ovex 
 |-  ( ( 0 ..^ K ) ^m ( 1 ... M ) ) e. _V
504 ovex 
 |-  ( ( 1 ... M ) ^m ( 1 ... M ) ) e. _V
505 f1of 
 |-  ( f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) -> f : ( 1 ... M ) --> ( 1 ... M ) )
506 505 ss2abi 
 |-  { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } C_ { f | f : ( 1 ... M ) --> ( 1 ... M ) }
507 68 68 mapval 
 |-  ( ( 1 ... M ) ^m ( 1 ... M ) ) = { f | f : ( 1 ... M ) --> ( 1 ... M ) }
508 506 507 sseqtrri 
 |-  { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } C_ ( ( 1 ... M ) ^m ( 1 ... M ) )
509 504 508 ssexi 
 |-  { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } e. _V
510 503 509 xpex 
 |-  ( ( ( 0 ..^ K ) ^m ( 1 ... M ) ) X. { f | f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) e. _V
511 510 rabex 
 |-  { 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 } e. _V
512 511 f1oen 
 |-  ( ( 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 ) >. } ) >. ) : { 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 } -1-1-onto-> { 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 ) ) } -> { 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 ) ) } )
513 502 512 syl 
 |-  ( 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 ) ) } )