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 syl5eq
 |-  ( 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 ) } ) ) )