Metamath Proof Explorer

Theorem poimirlem12

Description: Lemma for poimir connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem22.s 
|- S = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
poimirlem22.1 
|- ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
poimirlem12.2 
|- ( ph -> T e. S )
poimirlem12.3 
|- ( ph -> ( 2nd ` T ) = N )
poimirlem12.4 
|- ( ph -> U e. S )
poimirlem12.5 
|- ( ph -> ( 2nd ` U ) = N )
poimirlem12.6 
|- ( ph -> M e. ( 0 ... ( N - 1 ) ) )
Assertion poimirlem12 
|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) C_ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem22.s 
 |-  S = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
3 poimirlem22.1 
 |-  ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
4 poimirlem12.2 
 |-  ( ph -> T e. S )
5 poimirlem12.3 
 |-  ( ph -> ( 2nd ` T ) = N )
6 poimirlem12.4 
 |-  ( ph -> U e. S )
7 poimirlem12.5 
 |-  ( ph -> ( 2nd ` U ) = N )
8 poimirlem12.6 
 |-  ( ph -> M e. ( 0 ... ( N - 1 ) ) )
9 eldif 
 |-  ( y e. ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) <-> ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) )
10 imassrn 
 |-  ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) C_ ran ( 2nd ` ( 1st ` T ) )
11 elrabi 
 |-  ( T e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
12 11 2 eleq2s 
 |-  ( T e. S -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
13 xp1st 
 |-  ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
14 4 12 13 3syl 
 |-  ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
15 xp2nd 
 |-  ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
16 14 15 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
17 fvex 
 |-  ( 2nd ` ( 1st ` T ) ) e. _V
18 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
19 17 18 elab 
 |-  ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
20 16 19 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
21 f1of 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
22 frn 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 1 ... N ) -> ran ( 2nd ` ( 1st ` T ) ) C_ ( 1 ... N ) )
23 20 21 22 3syl 
 |-  ( ph -> ran ( 2nd ` ( 1st ` T ) ) C_ ( 1 ... N ) )
24 10 23 sstrid 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) C_ ( 1 ... N ) )
25 elrabi 
 |-  ( U e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } -> U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
26 25 2 eleq2s 
 |-  ( U e. S -> U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
27 xp1st 
 |-  ( U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` U ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
28 6 26 27 3syl 
 |-  ( ph -> ( 1st ` U ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
29 xp2nd 
 |-  ( ( 1st ` U ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` U ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
30 28 29 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
31 fvex 
 |-  ( 2nd ` ( 1st ` U ) ) e. _V
32 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` U ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
33 31 32 elab 
 |-  ( ( 2nd ` ( 1st ` U ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
34 30 33 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
35 f1ofo 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
36 foima 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
37 34 35 36 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
38 24 37 sseqtrrd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) C_ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) )
39 38 ssdifd 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) C_ ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) )
40 dff1o3 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` U ) ) ) )
41 40 simprbi 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` U ) ) )
42 imadif 
 |-  ( Fun `' ( 2nd ` ( 1st ` U ) ) -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ ( 1 ... M ) ) ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) )
43 34 41 42 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ ( 1 ... M ) ) ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) )
44 difun2 
 |-  ( ( ( ( M + 1 ) ... N ) u. ( 1 ... M ) ) \ ( 1 ... M ) ) = ( ( ( M + 1 ) ... N ) \ ( 1 ... M ) )
45 elfznn0 
 |-  ( M e. ( 0 ... ( N - 1 ) ) -> M e. NN0 )
46 nn0p1nn 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN )
47 8 45 46 3syl 
 |-  ( ph -> ( M + 1 ) e. NN )
48 nnuz 
 |-  NN = ( ZZ>= ` 1 )
49 47 48 eleqtrdi 
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` 1 ) )
50 1 nncnd 
 |-  ( ph -> N e. CC )
51 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
52 50 51 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
53 elfzuz3 
 |-  ( M e. ( 0 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
54 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` M ) )
55 8 53 54 3syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` M ) )
56 52 55 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
57 fzsplit2 
 |-  ( ( ( M + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` M ) ) -> ( 1 ... N ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) )
58 49 56 57 syl2anc 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) )
59 uncom 
 |-  ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) = ( ( ( M + 1 ) ... N ) u. ( 1 ... M ) )
60 58 59 eqtrdi 
 |-  ( ph -> ( 1 ... N ) = ( ( ( M + 1 ) ... N ) u. ( 1 ... M ) ) )
61 60 difeq1d 
 |-  ( ph -> ( ( 1 ... N ) \ ( 1 ... M ) ) = ( ( ( ( M + 1 ) ... N ) u. ( 1 ... M ) ) \ ( 1 ... M ) ) )
62 incom 
 |-  ( ( ( M + 1 ) ... N ) i^i ( 1 ... M ) ) = ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) )
63 8 45 syl 
 |-  ( ph -> M e. NN0 )
64 63 nn0red 
 |-  ( ph -> M e. RR )
65 64 ltp1d 
 |-  ( ph -> M < ( M + 1 ) )
66 fzdisj 
 |-  ( M < ( M + 1 ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
67 65 66 syl 
 |-  ( ph -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
68 62 67 syl5eq 
 |-  ( ph -> ( ( ( M + 1 ) ... N ) i^i ( 1 ... M ) ) = (/) )
69 disj3 
 |-  ( ( ( ( M + 1 ) ... N ) i^i ( 1 ... M ) ) = (/) <-> ( ( M + 1 ) ... N ) = ( ( ( M + 1 ) ... N ) \ ( 1 ... M ) ) )
70 68 69 sylib 
 |-  ( ph -> ( ( M + 1 ) ... N ) = ( ( ( M + 1 ) ... N ) \ ( 1 ... M ) ) )
71 44 61 70 3eqtr4a 
 |-  ( ph -> ( ( 1 ... N ) \ ( 1 ... M ) ) = ( ( M + 1 ) ... N ) )
72 71 imaeq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ ( 1 ... M ) ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
73 43 72 eqtr3d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
74 39 73 sseqtrd 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) C_ ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
75 74 sselda 
 |-  ( ( ph /\ y e. ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) ) -> y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
76 9 75 sylan2br 
 |-  ( ( ph /\ ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) ) -> y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
77 fveq2 
 |-  ( t = U -> ( 2nd ` t ) = ( 2nd ` U ) )
78 77 breq2d 
 |-  ( t = U -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` U ) ) )
79 78 ifbid 
 |-  ( t = U -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) )
80 79 csbeq1d 
 |-  ( t = U -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
81 2fveq3 
 |-  ( t = U -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` U ) ) )
82 2fveq3 
 |-  ( t = U -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` U ) ) )
83 82 imaeq1d 
 |-  ( t = U -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) )
84 83 xpeq1d 
 |-  ( t = U -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) )
85 82 imaeq1d 
 |-  ( t = U -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) )
86 85 xpeq1d 
 |-  ( t = U -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
87 84 86 uneq12d 
 |-  ( t = U -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
88 81 87 oveq12d 
 |-  ( t = U -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
89 88 csbeq2dv 
 |-  ( t = U -> [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
90 80 89 eqtrd 
 |-  ( t = U -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
91 90 mpteq2dv 
 |-  ( t = U -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
92 91 eqeq2d 
 |-  ( t = U -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
93 92 2 elrab2 
 |-  ( U e. S <-> ( U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
94 93 simprbi 
 |-  ( U e. S -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
95 6 94 syl 
 |-  ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
96 breq1 
 |-  ( y = M -> ( y < ( 2nd ` U ) <-> M < ( 2nd ` U ) ) )
97 id 
 |-  ( y = M -> y = M )
98 96 97 ifbieq1d 
 |-  ( y = M -> if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) = if ( M < ( 2nd ` U ) , M , ( y + 1 ) ) )
99 1 nnred 
 |-  ( ph -> N e. RR )
100 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
101 99 100 syl 
 |-  ( ph -> ( N - 1 ) e. RR )
102 elfzle2 
 |-  ( M e. ( 0 ... ( N - 1 ) ) -> M <_ ( N - 1 ) )
103 8 102 syl 
 |-  ( ph -> M <_ ( N - 1 ) )
104 99 ltm1d 
 |-  ( ph -> ( N - 1 ) < N )
105 64 101 99 103 104 lelttrd 
 |-  ( ph -> M < N )
106 105 7 breqtrrd 
 |-  ( ph -> M < ( 2nd ` U ) )
107 106 iftrued 
 |-  ( ph -> if ( M < ( 2nd ` U ) , M , ( y + 1 ) ) = M )
108 98 107 sylan9eqr 
 |-  ( ( ph /\ y = M ) -> if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) = M )
109 108 csbeq1d 
 |-  ( ( ph /\ y = M ) -> [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ M / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
110 oveq2 
 |-  ( j = M -> ( 1 ... j ) = ( 1 ... M ) )
111 110 imaeq2d 
 |-  ( j = M -> ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) )
112 111 xpeq1d 
 |-  ( j = M -> ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) )
113 oveq1 
 |-  ( j = M -> ( j + 1 ) = ( M + 1 ) )
114 113 oveq1d 
 |-  ( j = M -> ( ( j + 1 ) ... N ) = ( ( M + 1 ) ... N ) )
115 114 imaeq2d 
 |-  ( j = M -> ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
116 115 xpeq1d 
 |-  ( j = M -> ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) )
117 112 116 uneq12d 
 |-  ( j = M -> ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) )
118 117 oveq2d 
 |-  ( j = M -> ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
119 118 adantl 
 |-  ( ( ph /\ j = M ) -> ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
120 8 119 csbied 
 |-  ( ph -> [_ M / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
121 120 adantr 
 |-  ( ( ph /\ y = M ) -> [_ M / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
122 109 121 eqtrd 
 |-  ( ( ph /\ y = M ) -> [_ if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
123 ovexd 
 |-  ( ph -> ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V )
124 95 122 8 123 fvmptd 
 |-  ( ph -> ( F ` M ) = ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
125 124 fveq1d 
 |-  ( ph -> ( ( F ` M ) ` y ) = ( ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` y ) )
126 125 adantr 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( F ` M ) ` y ) = ( ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` y ) )
127 imassrn 
 |-  ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) C_ ran ( 2nd ` ( 1st ` U ) )
128 f1of 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) --> ( 1 ... N ) )
129 frn 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) --> ( 1 ... N ) -> ran ( 2nd ` ( 1st ` U ) ) C_ ( 1 ... N ) )
130 34 128 129 3syl 
 |-  ( ph -> ran ( 2nd ` ( 1st ` U ) ) C_ ( 1 ... N ) )
131 127 130 sstrid 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) C_ ( 1 ... N ) )
132 131 sselda 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> y e. ( 1 ... N ) )
133 xp1st 
 |-  ( ( 1st ` U ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( 1st ` U ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
134 elmapfn 
 |-  ( ( 1st ` ( 1st ` U ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` U ) ) Fn ( 1 ... N ) )
135 28 133 134 3syl 
 |-  ( ph -> ( 1st ` ( 1st ` U ) ) Fn ( 1 ... N ) )
136 135 adantr 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( 1st ` ( 1st ` U ) ) Fn ( 1 ... N ) )
137 1ex 
 |-  1 e. _V
138 fnconstg 
 |-  ( 1 e. _V -> ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) )
139 137 138 ax-mp 
 |-  ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) )
140 c0ex 
 |-  0 e. _V
141 fnconstg 
 |-  ( 0 e. _V -> ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
142 140 141 ax-mp 
 |-  ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) )
143 139 142 pm3.2i 
 |-  ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
144 imain 
 |-  ( Fun `' ( 2nd ` ( 1st ` U ) ) -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) )
145 34 41 144 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) )
146 67 imaeq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` U ) ) " (/) ) )
147 ima0 
 |-  ( ( 2nd ` ( 1st ` U ) ) " (/) ) = (/)
148 146 147 eqtrdi 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = (/) )
149 145 148 eqtr3d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) = (/) )
150 fnun 
 |-  ( ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) /\ ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) )
151 143 149 150 sylancr 
 |-  ( ph -> ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) )
152 imaundi 
 |-  ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) )
153 58 imaeq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) ) )
154 153 37 eqtr3d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) ) = ( 1 ... N ) )
155 152 154 eqtr3id 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) = ( 1 ... N ) )
156 155 fneq2d 
 |-  ( ph -> ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) <-> ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
157 151 156 mpbid 
 |-  ( ph -> ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
158 157 adantr 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
159 ovexd 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( 1 ... N ) e. _V )
160 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
161 eqidd 
 |-  ( ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` U ) ) ` y ) = ( ( 1st ` ( 1st ` U ) ) ` y ) )
162 fvun2 
 |-  ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) /\ ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) = (/) /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = ( ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ` y ) )
163 139 142 162 mp3an12 
 |-  ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) = (/) /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = ( ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ` y ) )
164 149 163 sylan 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = ( ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ` y ) )
165 140 fvconst2 
 |-  ( y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) -> ( ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ` y ) = 0 )
166 165 adantl 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ` y ) = 0 )
167 164 166 eqtrd 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = 0 )
168 167 adantr 
 |-  ( ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) /\ y e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = 0 )
169 136 158 159 159 160 161 168 ofval 
 |-  ( ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) /\ y e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` y ) = ( ( ( 1st ` ( 1st ` U ) ) ` y ) + 0 ) )
170 132 169 mpdan 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( ( 1st ` ( 1st ` U ) ) oF + ( ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` y ) = ( ( ( 1st ` ( 1st ` U ) ) ` y ) + 0 ) )
171 elmapi 
 |-  ( ( 1st ` ( 1st ` U ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` U ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
172 28 133 171 3syl 
 |-  ( ph -> ( 1st ` ( 1st ` U ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
173 172 ffvelrnda 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` U ) ) ` y ) e. ( 0 ..^ K ) )
174 elfzonn0 
 |-  ( ( ( 1st ` ( 1st ` U ) ) ` y ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` U ) ) ` y ) e. NN0 )
175 173 174 syl 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` U ) ) ` y ) e. NN0 )
176 175 nn0cnd 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` U ) ) ` y ) e. CC )
177 176 addid1d 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` U ) ) ` y ) + 0 ) = ( ( 1st ` ( 1st ` U ) ) ` y ) )
178 132 177 syldan 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( ( 1st ` ( 1st ` U ) ) ` y ) + 0 ) = ( ( 1st ` ( 1st ` U ) ) ` y ) )
179 126 170 178 3eqtrd 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` U ) ) " ( ( M + 1 ) ... N ) ) ) -> ( ( F ` M ) ` y ) = ( ( 1st ` ( 1st ` U ) ) ` y ) )
180 76 179 syldan 
 |-  ( ( ph /\ ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) ) -> ( ( F ` M ) ` y ) = ( ( 1st ` ( 1st ` U ) ) ` y ) )
181 fveq2 
 |-  ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
182 181 breq2d 
 |-  ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
183 182 ifbid 
 |-  ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
184 183 csbeq1d 
 |-  ( t = T -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
185 2fveq3 
 |-  ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
186 2fveq3 
 |-  ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
187 186 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
188 187 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
189 186 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
190 189 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
191 188 190 uneq12d 
 |-  ( t = T -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
192 185 191 oveq12d 
 |-  ( t = T -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
193 192 csbeq2dv 
 |-  ( t = T -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
194 184 193 eqtrd 
 |-  ( t = T -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
195 194 mpteq2dv 
 |-  ( t = T -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
196 195 eqeq2d 
 |-  ( t = T -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
197 196 2 elrab2 
 |-  ( T e. S <-> ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
198 197 simprbi 
 |-  ( T e. S -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
199 4 198 syl 
 |-  ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
200 breq1 
 |-  ( y = M -> ( y < ( 2nd ` T ) <-> M < ( 2nd ` T ) ) )
201 200 97 ifbieq1d 
 |-  ( y = M -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = if ( M < ( 2nd ` T ) , M , ( y + 1 ) ) )
202 105 5 breqtrrd 
 |-  ( ph -> M < ( 2nd ` T ) )
203 202 iftrued 
 |-  ( ph -> if ( M < ( 2nd ` T ) , M , ( y + 1 ) ) = M )
204 201 203 sylan9eqr 
 |-  ( ( ph /\ y = M ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = M )
205 204 csbeq1d 
 |-  ( ( ph /\ y = M ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ M / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
206 110 imaeq2d 
 |-  ( j = M -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) )
207 206 xpeq1d 
 |-  ( j = M -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) )
208 114 imaeq2d 
 |-  ( j = M -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
209 208 xpeq1d 
 |-  ( j = M -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) )
210 207 209 uneq12d 
 |-  ( j = M -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) )
211 210 oveq2d 
 |-  ( j = M -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
212 211 adantl 
 |-  ( ( ph /\ j = M ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
213 8 212 csbied 
 |-  ( ph -> [_ M / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
214 213 adantr 
 |-  ( ( ph /\ y = M ) -> [_ M / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
215 205 214 eqtrd 
 |-  ( ( ph /\ y = M ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
216 ovexd 
 |-  ( ph -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V )
217 199 215 8 216 fvmptd 
 |-  ( ph -> ( F ` M ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
218 217 fveq1d 
 |-  ( ph -> ( ( F ` M ) ` y ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` y ) )
219 218 adantr 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( F ` M ) ` y ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` y ) )
220 24 sselda 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> y e. ( 1 ... N ) )
221 xp1st 
 |-  ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
222 elmapfn 
 |-  ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
223 14 221 222 3syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
224 223 adantr 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
225 fnconstg 
 |-  ( 1 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) )
226 137 225 ax-mp 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) )
227 fnconstg 
 |-  ( 0 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
228 140 227 ax-mp 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) )
229 226 228 pm3.2i 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
230 dff1o3 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` T ) ) ) )
231 230 simprbi 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` T ) ) )
232 imain 
 |-  ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
233 20 231 232 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
234 67 imaeq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
235 ima0 
 |-  ( ( 2nd ` ( 1st ` T ) ) " (/) ) = (/)
236 234 235 eqtrdi 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = (/) )
237 233 236 eqtr3d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) )
238 fnun 
 |-  ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
239 229 237 238 sylancr 
 |-  ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
240 imaundi 
 |-  ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
241 58 imaeq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) ) )
242 f1ofo 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
243 foima 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
244 20 242 243 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
245 241 244 eqtr3d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) ) = ( 1 ... N ) )
246 240 245 eqtr3id 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = ( 1 ... N ) )
247 246 fneq2d 
 |-  ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) <-> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
248 239 247 mpbid 
 |-  ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
249 248 adantr 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
250 ovexd 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( 1 ... N ) e. _V )
251 eqidd 
 |-  ( ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` y ) = ( ( 1st ` ( 1st ` T ) ) ` y ) )
252 fvun1 
 |-  ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) /\ ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` y ) )
253 226 228 252 mp3an12 
 |-  ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` y ) )
254 237 253 sylan 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` y ) )
255 137 fvconst2 
 |-  ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` y ) = 1 )
256 255 adantl 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` y ) = 1 )
257 254 256 eqtrd 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = 1 )
258 257 adantr 
 |-  ( ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) /\ y e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` y ) = 1 )
259 224 249 250 250 160 251 258 ofval 
 |-  ( ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) /\ y e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` y ) = ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) )
260 220 259 mpdan 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` y ) = ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) )
261 219 260 eqtrd 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( F ` M ) ` y ) = ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) )
262 261 adantrr 
 |-  ( ( ph /\ ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) ) -> ( ( F ` M ) ` y ) = ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) )
263 1 nngt0d 
 |-  ( ph -> 0 < N )
264 263 7 breqtrrd 
 |-  ( ph -> 0 < ( 2nd ` U ) )
265 1 2 6 264 poimirlem5 
 |-  ( ph -> ( F ` 0 ) = ( 1st ` ( 1st ` U ) ) )
266 263 5 breqtrrd 
 |-  ( ph -> 0 < ( 2nd ` T ) )
267 1 2 4 266 poimirlem5 
 |-  ( ph -> ( F ` 0 ) = ( 1st ` ( 1st ` T ) ) )
268 265 267 eqtr3d 
 |-  ( ph -> ( 1st ` ( 1st ` U ) ) = ( 1st ` ( 1st ` T ) ) )
269 268 fveq1d 
 |-  ( ph -> ( ( 1st ` ( 1st ` U ) ) ` y ) = ( ( 1st ` ( 1st ` T ) ) ` y ) )
270 269 adantr 
 |-  ( ( ph /\ ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) ) -> ( ( 1st ` ( 1st ` U ) ) ` y ) = ( ( 1st ` ( 1st ` T ) ) ` y ) )
271 180 262 270 3eqtr3d 
 |-  ( ( ph /\ ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) = ( ( 1st ` ( 1st ` T ) ) ` y ) )
272 elmapi 
 |-  ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
273 14 221 272 3syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
274 273 ffvelrnda 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` y ) e. ( 0 ..^ K ) )
275 elfzonn0 
 |-  ( ( ( 1st ` ( 1st ` T ) ) ` y ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` y ) e. NN0 )
276 274 275 syl 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` y ) e. NN0 )
277 276 nn0red 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` y ) e. RR )
278 277 ltp1d 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` y ) < ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) )
279 277 278 gtned 
 |-  ( ( ph /\ y e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) =/= ( ( 1st ` ( 1st ` T ) ) ` y ) )
280 220 279 syldan 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) =/= ( ( 1st ` ( 1st ` T ) ) ` y ) )
281 280 neneqd 
 |-  ( ( ph /\ y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> -. ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) = ( ( 1st ` ( 1st ` T ) ) ` y ) )
282 281 adantrr 
 |-  ( ( ph /\ ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) ) -> -. ( ( ( 1st ` ( 1st ` T ) ) ` y ) + 1 ) = ( ( 1st ` ( 1st ` T ) ) ` y ) )
283 271 282 pm2.65da 
 |-  ( ph -> -. ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) )
284 iman 
 |-  ( ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) -> y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) <-> -. ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ -. y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) )
285 283 284 sylibr 
 |-  ( ph -> ( y e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) -> y e. ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) ) )
286 285 ssrdv 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) C_ ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... M ) ) )