Metamath Proof Explorer

Theorem poimirlem8

Description: Lemma for poimir , establishing that away from the opposite vertex the walks in poimirlem9 yield the same vertices. (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 } ) ) ) ) }
poimirlem9.1 
|- ( ph -> T e. S )
poimirlem9.2 
|- ( ph -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
poimirlem9.3 
|- ( ph -> U e. S )
Assertion poimirlem8 
|- ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )

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 poimirlem9.1 
 |-  ( ph -> T e. S )
4 poimirlem9.2 
 |-  ( ph -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
5 poimirlem9.3 
 |-  ( ph -> U e. S )
6 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 ) ) )
7 6 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 ) ) )
8 5 7 syl 
 |-  ( ph -> U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
9 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 ) } ) )
10 8 9 syl 
 |-  ( ph -> ( 1st ` U ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
11 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 ) } )
12 10 11 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
13 fvex 
 |-  ( 2nd ` ( 1st ` U ) ) e. _V
14 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` U ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
15 13 14 elab 
 |-  ( ( 2nd ` ( 1st ` U ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
16 12 15 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
17 f1ofn 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` U ) ) Fn ( 1 ... N ) )
18 16 17 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) Fn ( 1 ... N ) )
19 difss 
 |-  ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( 1 ... N )
20 fnssres 
 |-  ( ( ( 2nd ` ( 1st ` U ) ) Fn ( 1 ... N ) /\ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) Fn ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
21 18 19 20 sylancl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) Fn ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
22 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 ) ) )
23 22 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 ) ) )
24 3 23 syl 
 |-  ( ph -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
25 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 ) } ) )
26 24 25 syl 
 |-  ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
27 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 ) } )
28 26 27 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
29 fvex 
 |-  ( 2nd ` ( 1st ` T ) ) e. _V
30 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
31 29 30 elab 
 |-  ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
32 28 31 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
33 f1ofn 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
34 32 33 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
35 fnssres 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) Fn ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
36 34 19 35 sylancl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) Fn ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
37 fzp1elp1 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
38 4 37 syl 
 |-  ( ph -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
39 1 nncnd 
 |-  ( ph -> N e. CC )
40 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
41 39 40 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
42 41 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
43 38 42 eleqtrd 
 |-  ( ph -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) )
44 fzsplit 
 |-  ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) -> ( 1 ... N ) = ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
45 43 44 syl 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
46 45 difeq1d 
 |-  ( ph -> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
47 difundir 
 |-  ( ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
48 elfznn 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) e. NN )
49 4 48 syl 
 |-  ( ph -> ( 2nd ` T ) e. NN )
50 49 nncnd 
 |-  ( ph -> ( 2nd ` T ) e. CC )
51 npcan1 
 |-  ( ( 2nd ` T ) e. CC -> ( ( ( 2nd ` T ) - 1 ) + 1 ) = ( 2nd ` T ) )
52 50 51 syl 
 |-  ( ph -> ( ( ( 2nd ` T ) - 1 ) + 1 ) = ( 2nd ` T ) )
53 nnuz 
 |-  NN = ( ZZ>= ` 1 )
54 49 53 eleqtrdi 
 |-  ( ph -> ( 2nd ` T ) e. ( ZZ>= ` 1 ) )
55 52 54 eqeltrd 
 |-  ( ph -> ( ( ( 2nd ` T ) - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
56 49 nnzd 
 |-  ( ph -> ( 2nd ` T ) e. ZZ )
57 peano2zm 
 |-  ( ( 2nd ` T ) e. ZZ -> ( ( 2nd ` T ) - 1 ) e. ZZ )
58 56 57 syl 
 |-  ( ph -> ( ( 2nd ` T ) - 1 ) e. ZZ )
59 uzid 
 |-  ( ( ( 2nd ` T ) - 1 ) e. ZZ -> ( ( 2nd ` T ) - 1 ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) )
60 peano2uz 
 |-  ( ( ( 2nd ` T ) - 1 ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) -> ( ( ( 2nd ` T ) - 1 ) + 1 ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) )
61 58 59 60 3syl 
 |-  ( ph -> ( ( ( 2nd ` T ) - 1 ) + 1 ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) )
62 52 61 eqeltrrd 
 |-  ( ph -> ( 2nd ` T ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) )
63 peano2uz 
 |-  ( ( 2nd ` T ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) -> ( ( 2nd ` T ) + 1 ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) )
64 62 63 syl 
 |-  ( ph -> ( ( 2nd ` T ) + 1 ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) )
65 fzsplit2 
 |-  ( ( ( ( ( 2nd ` T ) - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ ( ( 2nd ` T ) + 1 ) e. ( ZZ>= ` ( ( 2nd ` T ) - 1 ) ) ) -> ( 1 ... ( ( 2nd ` T ) + 1 ) ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. ( ( ( ( 2nd ` T ) - 1 ) + 1 ) ... ( ( 2nd ` T ) + 1 ) ) ) )
66 55 64 65 syl2anc 
 |-  ( ph -> ( 1 ... ( ( 2nd ` T ) + 1 ) ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. ( ( ( ( 2nd ` T ) - 1 ) + 1 ) ... ( ( 2nd ` T ) + 1 ) ) ) )
67 52 oveq1d 
 |-  ( ph -> ( ( ( ( 2nd ` T ) - 1 ) + 1 ) ... ( ( 2nd ` T ) + 1 ) ) = ( ( 2nd ` T ) ... ( ( 2nd ` T ) + 1 ) ) )
68 fzpr 
 |-  ( ( 2nd ` T ) e. ZZ -> ( ( 2nd ` T ) ... ( ( 2nd ` T ) + 1 ) ) = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
69 56 68 syl 
 |-  ( ph -> ( ( 2nd ` T ) ... ( ( 2nd ` T ) + 1 ) ) = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
70 67 69 eqtrd 
 |-  ( ph -> ( ( ( ( 2nd ` T ) - 1 ) + 1 ) ... ( ( 2nd ` T ) + 1 ) ) = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
71 70 uneq2d 
 |-  ( ph -> ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. ( ( ( ( 2nd ` T ) - 1 ) + 1 ) ... ( ( 2nd ` T ) + 1 ) ) ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
72 66 71 eqtrd 
 |-  ( ph -> ( 1 ... ( ( 2nd ` T ) + 1 ) ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
73 72 difeq1d 
 |-  ( ph -> ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
74 49 nnred 
 |-  ( ph -> ( 2nd ` T ) e. RR )
75 74 ltm1d 
 |-  ( ph -> ( ( 2nd ` T ) - 1 ) < ( 2nd ` T ) )
76 58 zred 
 |-  ( ph -> ( ( 2nd ` T ) - 1 ) e. RR )
77 76 74 ltnled 
 |-  ( ph -> ( ( ( 2nd ` T ) - 1 ) < ( 2nd ` T ) <-> -. ( 2nd ` T ) <_ ( ( 2nd ` T ) - 1 ) ) )
78 75 77 mpbid 
 |-  ( ph -> -. ( 2nd ` T ) <_ ( ( 2nd ` T ) - 1 ) )
79 elfzle2 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) -> ( 2nd ` T ) <_ ( ( 2nd ` T ) - 1 ) )
80 78 79 nsyl 
 |-  ( ph -> -. ( 2nd ` T ) e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
81 difsn 
 |-  ( -. ( 2nd ` T ) e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) -> ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( 2nd ` T ) } ) = ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
82 80 81 syl 
 |-  ( ph -> ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( 2nd ` T ) } ) = ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
83 peano2re 
 |-  ( ( 2nd ` T ) e. RR -> ( ( 2nd ` T ) + 1 ) e. RR )
84 74 83 syl 
 |-  ( ph -> ( ( 2nd ` T ) + 1 ) e. RR )
85 74 ltp1d 
 |-  ( ph -> ( 2nd ` T ) < ( ( 2nd ` T ) + 1 ) )
86 76 74 84 75 85 lttrd 
 |-  ( ph -> ( ( 2nd ` T ) - 1 ) < ( ( 2nd ` T ) + 1 ) )
87 76 84 ltnled 
 |-  ( ph -> ( ( ( 2nd ` T ) - 1 ) < ( ( 2nd ` T ) + 1 ) <-> -. ( ( 2nd ` T ) + 1 ) <_ ( ( 2nd ` T ) - 1 ) ) )
88 86 87 mpbid 
 |-  ( ph -> -. ( ( 2nd ` T ) + 1 ) <_ ( ( 2nd ` T ) - 1 ) )
89 elfzle2 
 |-  ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) -> ( ( 2nd ` T ) + 1 ) <_ ( ( 2nd ` T ) - 1 ) )
90 88 89 nsyl 
 |-  ( ph -> -. ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
91 difsn 
 |-  ( -. ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) -> ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( ( 2nd ` T ) + 1 ) } ) = ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
92 90 91 syl 
 |-  ( ph -> ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( ( 2nd ` T ) + 1 ) } ) = ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
93 82 92 ineq12d 
 |-  ( ph -> ( ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( 2nd ` T ) } ) i^i ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) i^i ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) )
94 difun2 
 |-  ( ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
95 df-pr 
 |-  { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } = ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } )
96 95 difeq2i 
 |-  ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) )
97 difundi 
 |-  ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( 2nd ` T ) } ) i^i ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( ( 2nd ` T ) + 1 ) } ) )
98 94 96 97 3eqtrri 
 |-  ( ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( 2nd ` T ) } ) i^i ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) \ { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
99 inidm 
 |-  ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) i^i ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) = ( 1 ... ( ( 2nd ` T ) - 1 ) )
100 93 98 99 3eqtr3g 
 |-  ( ph -> ( ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
101 73 100 eqtrd 
 |-  ( ph -> ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
102 peano2re 
 |-  ( ( ( 2nd ` T ) + 1 ) e. RR -> ( ( ( 2nd ` T ) + 1 ) + 1 ) e. RR )
103 84 102 syl 
 |-  ( ph -> ( ( ( 2nd ` T ) + 1 ) + 1 ) e. RR )
104 84 ltp1d 
 |-  ( ph -> ( ( 2nd ` T ) + 1 ) < ( ( ( 2nd ` T ) + 1 ) + 1 ) )
105 74 84 103 85 104 lttrd 
 |-  ( ph -> ( 2nd ` T ) < ( ( ( 2nd ` T ) + 1 ) + 1 ) )
106 74 103 ltnled 
 |-  ( ph -> ( ( 2nd ` T ) < ( ( ( 2nd ` T ) + 1 ) + 1 ) <-> -. ( ( ( 2nd ` T ) + 1 ) + 1 ) <_ ( 2nd ` T ) ) )
107 105 106 mpbid 
 |-  ( ph -> -. ( ( ( 2nd ` T ) + 1 ) + 1 ) <_ ( 2nd ` T ) )
108 elfzle1 
 |-  ( ( 2nd ` T ) e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) -> ( ( ( 2nd ` T ) + 1 ) + 1 ) <_ ( 2nd ` T ) )
109 107 108 nsyl 
 |-  ( ph -> -. ( 2nd ` T ) e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
110 difsn 
 |-  ( -. ( 2nd ` T ) e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) -> ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) } ) = ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
111 109 110 syl 
 |-  ( ph -> ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) } ) = ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
112 84 103 ltnled 
 |-  ( ph -> ( ( ( 2nd ` T ) + 1 ) < ( ( ( 2nd ` T ) + 1 ) + 1 ) <-> -. ( ( ( 2nd ` T ) + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) ) )
113 104 112 mpbid 
 |-  ( ph -> -. ( ( ( 2nd ` T ) + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) )
114 elfzle1 
 |-  ( ( ( 2nd ` T ) + 1 ) e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) -> ( ( ( 2nd ` T ) + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) )
115 113 114 nsyl 
 |-  ( ph -> -. ( ( 2nd ` T ) + 1 ) e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
116 difsn 
 |-  ( -. ( ( 2nd ` T ) + 1 ) e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) -> ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( ( 2nd ` T ) + 1 ) } ) = ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
117 115 116 syl 
 |-  ( ph -> ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( ( 2nd ` T ) + 1 ) } ) = ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
118 111 117 ineq12d 
 |-  ( ph -> ( ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) } ) i^i ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) i^i ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
119 95 difeq2i 
 |-  ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) )
120 difundi 
 |-  ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) } ) i^i ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( ( 2nd ` T ) + 1 ) } ) )
121 119 120 eqtr2i 
 |-  ( ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) } ) i^i ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
122 inidm 
 |-  ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) i^i ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) = ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N )
123 118 121 122 3eqtr3g 
 |-  ( ph -> ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
124 101 123 uneq12d 
 |-  ( ph -> ( ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
125 47 124 eqtrid 
 |-  ( ph -> ( ( ( 1 ... ( ( 2nd ` T ) + 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
126 46 125 eqtrd 
 |-  ( ph -> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
127 126 eleq2d 
 |-  ( ph -> ( k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) <-> k e. ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) ) )
128 elun 
 |-  ( k e. ( ( 1 ... ( ( 2nd ` T ) - 1 ) ) u. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) <-> ( k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) \/ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
129 127 128 bitrdi 
 |-  ( ph -> ( k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) <-> ( k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) \/ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) ) )
130 129 biimpa 
 |-  ( ( ph /\ k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) \/ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
131 fveq2 
 |-  ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
132 131 breq2d 
 |-  ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
133 132 ifbid 
 |-  ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
134 133 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 } ) ) ) )
135 2fveq3 
 |-  ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
136 2fveq3 
 |-  ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
137 136 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
138 137 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
139 136 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
140 139 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
141 138 140 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 } ) ) )
142 135 141 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 } ) ) ) )
143 142 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 } ) ) ) )
144 134 143 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 } ) ) ) )
145 144 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 } ) ) ) ) )
146 145 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 } ) ) ) ) ) )
147 146 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 } ) ) ) ) ) )
148 147 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 } ) ) ) ) )
149 3 148 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 } ) ) ) ) )
150 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 ) ) )
151 26 150 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
152 elmapi 
 |-  ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
153 151 152 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
154 elfzoelz 
 |-  ( n e. ( 0 ..^ K ) -> n e. ZZ )
155 154 ssriv 
 |-  ( 0 ..^ K ) C_ ZZ
156 fss 
 |-  ( ( ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) /\ ( 0 ..^ K ) C_ ZZ ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ZZ )
157 153 155 156 sylancl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ZZ )
158 1 149 157 32 4 poimirlem1 
 |-  ( ph -> -. E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) )
159 1 adantr 
 |-  ( ( ph /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) -> N e. NN )
160 fveq2 
 |-  ( t = U -> ( 2nd ` t ) = ( 2nd ` U ) )
161 160 breq2d 
 |-  ( t = U -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` U ) ) )
162 161 ifbid 
 |-  ( t = U -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` U ) , y , ( y + 1 ) ) )
163 162 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 } ) ) ) )
164 2fveq3 
 |-  ( t = U -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` U ) ) )
165 2fveq3 
 |-  ( t = U -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` U ) ) )
166 165 imaeq1d 
 |-  ( t = U -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) )
167 166 xpeq1d 
 |-  ( t = U -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... j ) ) X. { 1 } ) )
168 165 imaeq1d 
 |-  ( t = U -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) )
169 168 xpeq1d 
 |-  ( t = U -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
170 167 169 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 } ) ) )
171 164 170 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 } ) ) ) )
172 171 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 } ) ) ) )
173 163 172 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 } ) ) ) )
174 173 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 } ) ) ) ) )
175 174 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 } ) ) ) ) ) )
176 175 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 } ) ) ) ) ) )
177 176 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 } ) ) ) ) )
178 5 177 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 } ) ) ) ) )
179 178 adantr 
 |-  ( ( ph /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) -> 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 } ) ) ) ) )
180 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 ) ) )
181 10 180 syl 
 |-  ( ph -> ( 1st ` ( 1st ` U ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
182 elmapi 
 |-  ( ( 1st ` ( 1st ` U ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` U ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
183 181 182 syl 
 |-  ( ph -> ( 1st ` ( 1st ` U ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
184 fss 
 |-  ( ( ( 1st ` ( 1st ` U ) ) : ( 1 ... N ) --> ( 0 ..^ K ) /\ ( 0 ..^ K ) C_ ZZ ) -> ( 1st ` ( 1st ` U ) ) : ( 1 ... N ) --> ZZ )
185 183 155 184 sylancl 
 |-  ( ph -> ( 1st ` ( 1st ` U ) ) : ( 1 ... N ) --> ZZ )
186 185 adantr 
 |-  ( ( ph /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) -> ( 1st ` ( 1st ` U ) ) : ( 1 ... N ) --> ZZ )
187 16 adantr 
 |-  ( ( ph /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
188 4 adantr 
 |-  ( ( ph /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
189 xp2nd 
 |-  ( U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 2nd ` U ) e. ( 0 ... N ) )
190 8 189 syl 
 |-  ( ph -> ( 2nd ` U ) e. ( 0 ... N ) )
191 eldifsn 
 |-  ( ( 2nd ` U ) e. ( ( 0 ... N ) \ { ( 2nd ` T ) } ) <-> ( ( 2nd ` U ) e. ( 0 ... N ) /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) )
192 191 biimpri 
 |-  ( ( ( 2nd ` U ) e. ( 0 ... N ) /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) -> ( 2nd ` U ) e. ( ( 0 ... N ) \ { ( 2nd ` T ) } ) )
193 190 192 sylan 
 |-  ( ( ph /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) -> ( 2nd ` U ) e. ( ( 0 ... N ) \ { ( 2nd ` T ) } ) )
194 159 179 186 187 188 193 poimirlem2 
 |-  ( ( ph /\ ( 2nd ` U ) =/= ( 2nd ` T ) ) -> E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) )
195 194 ex 
 |-  ( ph -> ( ( 2nd ` U ) =/= ( 2nd ` T ) -> E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) ) )
196 195 necon1bd 
 |-  ( ph -> ( -. E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) -> ( 2nd ` U ) = ( 2nd ` T ) ) )
197 158 196 mpd 
 |-  ( ph -> ( 2nd ` U ) = ( 2nd ` T ) )
198 197 oveq1d 
 |-  ( ph -> ( ( 2nd ` U ) - 1 ) = ( ( 2nd ` T ) - 1 ) )
199 198 oveq2d 
 |-  ( ph -> ( 1 ... ( ( 2nd ` U ) - 1 ) ) = ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
200 199 eleq2d 
 |-  ( ph -> ( k e. ( 1 ... ( ( 2nd ` U ) - 1 ) ) <-> k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) )
201 200 biimpar 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) -> k e. ( 1 ... ( ( 2nd ` U ) - 1 ) ) )
202 1 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` U ) - 1 ) ) ) -> N e. NN )
203 5 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` U ) - 1 ) ) ) -> U e. S )
204 197 4 eqeltrd 
 |-  ( ph -> ( 2nd ` U ) e. ( 1 ... ( N - 1 ) ) )
205 204 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` U ) - 1 ) ) ) -> ( 2nd ` U ) e. ( 1 ... ( N - 1 ) ) )
206 simpr 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` U ) - 1 ) ) ) -> k e. ( 1 ... ( ( 2nd ` U ) - 1 ) ) )
207 202 2 203 205 206 poimirlem6 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` U ) - 1 ) ) ) -> ( iota_ n e. ( 1 ... N ) ( ( F ` ( k - 1 ) ) ` n ) =/= ( ( F ` k ) ` n ) ) = ( ( 2nd ` ( 1st ` U ) ) ` k ) )
208 201 207 syldan 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) -> ( iota_ n e. ( 1 ... N ) ( ( F ` ( k - 1 ) ) ` n ) =/= ( ( F ` k ) ` n ) ) = ( ( 2nd ` ( 1st ` U ) ) ` k ) )
209 1 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) -> N e. NN )
210 3 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) -> T e. S )
211 4 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
212 simpr 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) -> k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) )
213 209 2 210 211 212 poimirlem6 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) -> ( iota_ n e. ( 1 ... N ) ( ( F ` ( k - 1 ) ) ` n ) =/= ( ( F ` k ) ` n ) ) = ( ( 2nd ` ( 1st ` T ) ) ` k ) )
214 208 213 eqtr3d 
 |-  ( ( ph /\ k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) ) -> ( ( 2nd ` ( 1st ` U ) ) ` k ) = ( ( 2nd ` ( 1st ` T ) ) ` k ) )
215 197 oveq1d 
 |-  ( ph -> ( ( 2nd ` U ) + 1 ) = ( ( 2nd ` T ) + 1 ) )
216 215 oveq1d 
 |-  ( ph -> ( ( ( 2nd ` U ) + 1 ) + 1 ) = ( ( ( 2nd ` T ) + 1 ) + 1 ) )
217 216 oveq1d 
 |-  ( ph -> ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) = ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
218 217 eleq2d 
 |-  ( ph -> ( k e. ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) <-> k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) )
219 218 biimpar 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) -> k e. ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) )
220 1 adantr 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) ) -> N e. NN )
221 5 adantr 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) ) -> U e. S )
222 204 adantr 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) ) -> ( 2nd ` U ) e. ( 1 ... ( N - 1 ) ) )
223 simpr 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) ) -> k e. ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) )
224 220 2 221 222 223 poimirlem7 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` U ) + 1 ) + 1 ) ... N ) ) -> ( iota_ n e. ( 1 ... N ) ( ( F ` ( k - 2 ) ) ` n ) =/= ( ( F ` ( k - 1 ) ) ` n ) ) = ( ( 2nd ` ( 1st ` U ) ) ` k ) )
225 219 224 syldan 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) -> ( iota_ n e. ( 1 ... N ) ( ( F ` ( k - 2 ) ) ` n ) =/= ( ( F ` ( k - 1 ) ) ` n ) ) = ( ( 2nd ` ( 1st ` U ) ) ` k ) )
226 1 adantr 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) -> N e. NN )
227 3 adantr 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) -> T e. S )
228 4 adantr 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
229 simpr 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) -> k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
230 226 2 227 228 229 poimirlem7 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) -> ( iota_ n e. ( 1 ... N ) ( ( F ` ( k - 2 ) ) ` n ) =/= ( ( F ` ( k - 1 ) ) ` n ) ) = ( ( 2nd ` ( 1st ` T ) ) ` k ) )
231 225 230 eqtr3d 
 |-  ( ( ph /\ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) -> ( ( 2nd ` ( 1st ` U ) ) ` k ) = ( ( 2nd ` ( 1st ` T ) ) ` k ) )
232 214 231 jaodan 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( 2nd ` T ) - 1 ) ) \/ k e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) ) ) -> ( ( 2nd ` ( 1st ` U ) ) ` k ) = ( ( 2nd ` ( 1st ` T ) ) ` k ) )
233 130 232 syldan 
 |-  ( ( ph /\ k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( ( 2nd ` ( 1st ` U ) ) ` k ) = ( ( 2nd ` ( 1st ` T ) ) ` k ) )
234 fvres 
 |-  ( k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ` k ) = ( ( 2nd ` ( 1st ` U ) ) ` k ) )
235 234 adantl 
 |-  ( ( ph /\ k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ` k ) = ( ( 2nd ` ( 1st ` U ) ) ` k ) )
236 fvres 
 |-  ( k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ` k ) = ( ( 2nd ` ( 1st ` T ) ) ` k ) )
237 236 adantl 
 |-  ( ( ph /\ k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ` k ) = ( ( 2nd ` ( 1st ` T ) ) ` k ) )
238 233 235 237 3eqtr4d 
 |-  ( ( ph /\ k e. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ` k ) = ( ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ` k ) )
239 21 36 238 eqfnfvd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )