Metamath Proof Explorer

Theorem poimirlem11

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