Metamath Proof Explorer

Theorem poimirlem22

Description: Lemma for poimir , that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (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 ) ) )
poimirlem22.2 
|- ( ph -> T e. S )
poimirlem22.3 
|- ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= 0 )
poimirlem22.4 
|- ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= K )
Assertion poimirlem22 
|- ( ph -> E! z e. S z =/= T )

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 poimirlem22.2 
 |-  ( ph -> T e. S )
5 poimirlem22.3 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= 0 )
6 poimirlem22.4 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= K )
7 1 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> N e. NN )
8 3 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
9 4 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> T e. S )
10 simpr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
11 7 2 8 9 10 poimirlem15 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. e. S )
12 fveq2 
 |-  ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
13 12 breq2d 
 |-  ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
14 13 ifbid 
 |-  ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
15 14 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 } ) ) ) )
16 2fveq3 
 |-  ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
17 2fveq3 
 |-  ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
18 17 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
19 18 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
20 17 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
21 20 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
22 19 21 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 } ) ) )
23 16 22 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 } ) ) ) )
24 23 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 } ) ) ) )
25 15 24 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 } ) ) ) )
26 25 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 } ) ) ) ) )
27 26 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 } ) ) ) ) ) )
28 27 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 } ) ) ) ) ) )
29 28 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 } ) ) ) ) )
30 4 29 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 } ) ) ) ) )
31 30 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> 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 } ) ) ) ) )
32 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 ) ) )
33 32 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 ) ) )
34 4 33 syl 
 |-  ( ph -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
35 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 ) } ) )
36 34 35 syl 
 |-  ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
37 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 ) ) )
38 36 37 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
39 elmapi 
 |-  ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
40 38 39 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
41 elfzoelz 
 |-  ( n e. ( 0 ..^ K ) -> n e. ZZ )
42 41 ssriv 
 |-  ( 0 ..^ K ) C_ ZZ
43 fss 
 |-  ( ( ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) /\ ( 0 ..^ K ) C_ ZZ ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ZZ )
44 40 42 43 sylancl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ZZ )
45 44 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ZZ )
46 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 ) } )
47 36 46 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
48 fvex 
 |-  ( 2nd ` ( 1st ` T ) ) e. _V
49 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
50 48 49 elab 
 |-  ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
51 47 50 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
52 51 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
53 7 31 45 52 10 poimirlem1 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> -. E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) )
54 53 adantr 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> -. E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) )
55 1 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) -> N e. NN )
56 fveq2 
 |-  ( t = z -> ( 2nd ` t ) = ( 2nd ` z ) )
57 56 breq2d 
 |-  ( t = z -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` z ) ) )
58 57 ifbid 
 |-  ( t = z -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) )
59 58 csbeq1d 
 |-  ( t = z -> [_ 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 ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
60 2fveq3 
 |-  ( t = z -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` z ) ) )
61 2fveq3 
 |-  ( t = z -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` z ) ) )
62 61 imaeq1d 
 |-  ( t = z -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) )
63 62 xpeq1d 
 |-  ( t = z -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) )
64 61 imaeq1d 
 |-  ( t = z -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) )
65 64 xpeq1d 
 |-  ( t = z -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
66 63 65 uneq12d 
 |-  ( t = z -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
67 60 66 oveq12d 
 |-  ( t = z -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
68 67 csbeq2dv 
 |-  ( t = z -> [_ if ( y < ( 2nd ` z ) , 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 ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
69 59 68 eqtrd 
 |-  ( t = z -> [_ 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 ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
70 69 mpteq2dv 
 |-  ( t = z -> ( 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 ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
71 70 eqeq2d 
 |-  ( t = z -> ( 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 ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
72 71 2 elrab2 
 |-  ( z e. S <-> ( z 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 ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
73 72 simprbi 
 |-  ( z e. S -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
74 73 ad2antlr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
75 elrabi 
 |-  ( z 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 } ) ) ) ) } -> z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
76 75 2 eleq2s 
 |-  ( z e. S -> z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
77 xp1st 
 |-  ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
78 76 77 syl 
 |-  ( z e. S -> ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
79 xp1st 
 |-  ( ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( 1st ` z ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
80 78 79 syl 
 |-  ( z e. S -> ( 1st ` ( 1st ` z ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
81 elmapi 
 |-  ( ( 1st ` ( 1st ` z ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
82 80 81 syl 
 |-  ( z e. S -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
83 fss 
 |-  ( ( ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ( 0 ..^ K ) /\ ( 0 ..^ K ) C_ ZZ ) -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ZZ )
84 82 42 83 sylancl 
 |-  ( z e. S -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ZZ )
85 84 ad2antlr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ZZ )
86 xp2nd 
 |-  ( ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
87 78 86 syl 
 |-  ( z e. S -> ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
88 fvex 
 |-  ( 2nd ` ( 1st ` z ) ) e. _V
89 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` z ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
90 88 89 elab 
 |-  ( ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
91 87 90 sylib 
 |-  ( z e. S -> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
92 91 ad2antlr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) -> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
93 simpllr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
94 xp2nd 
 |-  ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 2nd ` z ) e. ( 0 ... N ) )
95 76 94 syl 
 |-  ( z e. S -> ( 2nd ` z ) e. ( 0 ... N ) )
96 95 adantl 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( 2nd ` z ) e. ( 0 ... N ) )
97 eldifsn 
 |-  ( ( 2nd ` z ) e. ( ( 0 ... N ) \ { ( 2nd ` T ) } ) <-> ( ( 2nd ` z ) e. ( 0 ... N ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) )
98 97 biimpri 
 |-  ( ( ( 2nd ` z ) e. ( 0 ... N ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) -> ( 2nd ` z ) e. ( ( 0 ... N ) \ { ( 2nd ` T ) } ) )
99 96 98 sylan 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) -> ( 2nd ` z ) e. ( ( 0 ... N ) \ { ( 2nd ` T ) } ) )
100 55 74 85 92 93 99 poimirlem2 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ ( 2nd ` z ) =/= ( 2nd ` T ) ) -> E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) )
101 100 ex 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( ( 2nd ` z ) =/= ( 2nd ` T ) -> E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) ) )
102 101 necon1bd 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( -. E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` T ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` T ) ) ` n ) -> ( 2nd ` z ) = ( 2nd ` T ) ) )
103 54 102 mpd 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( 2nd ` z ) = ( 2nd ` T ) )
104 eleq1 
 |-  ( ( 2nd ` z ) = ( 2nd ` T ) -> ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) <-> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) )
105 104 biimparc 
 |-  ( ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) -> ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) )
106 105 anim2i 
 |-  ( ( ph /\ ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) ) -> ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
107 106 anassrs 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) -> ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
108 73 adantl 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
109 breq1 
 |-  ( y = 0 -> ( y < ( 2nd ` z ) <-> 0 < ( 2nd ` z ) ) )
110 id 
 |-  ( y = 0 -> y = 0 )
111 109 110 ifbieq1d 
 |-  ( y = 0 -> if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) = if ( 0 < ( 2nd ` z ) , 0 , ( y + 1 ) ) )
112 elfznn 
 |-  ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` z ) e. NN )
113 112 nngt0d 
 |-  ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) -> 0 < ( 2nd ` z ) )
114 113 iftrued 
 |-  ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) -> if ( 0 < ( 2nd ` z ) , 0 , ( y + 1 ) ) = 0 )
115 114 ad2antlr 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> if ( 0 < ( 2nd ` z ) , 0 , ( y + 1 ) ) = 0 )
116 111 115 sylan9eqr 
 |-  ( ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ y = 0 ) -> if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) = 0 )
117 116 csbeq1d 
 |-  ( ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ y = 0 ) -> [_ if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ 0 / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
118 c0ex 
 |-  0 e. _V
119 oveq2 
 |-  ( j = 0 -> ( 1 ... j ) = ( 1 ... 0 ) )
120 fz10 
 |-  ( 1 ... 0 ) = (/)
121 119 120 eqtrdi 
 |-  ( j = 0 -> ( 1 ... j ) = (/) )
122 121 imaeq2d 
 |-  ( j = 0 -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` z ) ) " (/) ) )
123 122 xpeq1d 
 |-  ( j = 0 -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` z ) ) " (/) ) X. { 1 } ) )
124 oveq1 
 |-  ( j = 0 -> ( j + 1 ) = ( 0 + 1 ) )
125 0p1e1 
 |-  ( 0 + 1 ) = 1
126 124 125 eqtrdi 
 |-  ( j = 0 -> ( j + 1 ) = 1 )
127 126 oveq1d 
 |-  ( j = 0 -> ( ( j + 1 ) ... N ) = ( 1 ... N ) )
128 127 imaeq2d 
 |-  ( j = 0 -> ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) )
129 128 xpeq1d 
 |-  ( j = 0 -> ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) )
130 123 129 uneq12d 
 |-  ( j = 0 -> ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` z ) ) " (/) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) ) )
131 ima0 
 |-  ( ( 2nd ` ( 1st ` z ) ) " (/) ) = (/)
132 131 xpeq1i 
 |-  ( ( ( 2nd ` ( 1st ` z ) ) " (/) ) X. { 1 } ) = ( (/) X. { 1 } )
133 0xp 
 |-  ( (/) X. { 1 } ) = (/)
134 132 133 eqtri 
 |-  ( ( ( 2nd ` ( 1st ` z ) ) " (/) ) X. { 1 } ) = (/)
135 134 uneq1i 
 |-  ( ( ( ( 2nd ` ( 1st ` z ) ) " (/) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) ) = ( (/) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) )
136 uncom 
 |-  ( (/) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) u. (/) )
137 un0 
 |-  ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) u. (/) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } )
138 135 136 137 3eqtri 
 |-  ( ( ( ( 2nd ` ( 1st ` z ) ) " (/) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } )
139 130 138 eqtrdi 
 |-  ( j = 0 -> ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) )
140 139 oveq2d 
 |-  ( j = 0 -> ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) ) )
141 118 140 csbie 
 |-  [_ 0 / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) )
142 f1ofo 
 |-  ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
143 91 142 syl 
 |-  ( z e. S -> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
144 foima 
 |-  ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
145 143 144 syl 
 |-  ( z e. S -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
146 145 xpeq1d 
 |-  ( z e. S -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) = ( ( 1 ... N ) X. { 0 } ) )
147 146 oveq2d 
 |-  ( z e. S -> ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) ) = ( ( 1st ` ( 1st ` z ) ) oF + ( ( 1 ... N ) X. { 0 } ) ) )
148 ovexd 
 |-  ( z e. S -> ( 1 ... N ) e. _V )
149 82 ffnd 
 |-  ( z e. S -> ( 1st ` ( 1st ` z ) ) Fn ( 1 ... N ) )
150 fnconstg 
 |-  ( 0 e. _V -> ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N ) )
151 118 150 mp1i 
 |-  ( z e. S -> ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N ) )
152 eqidd 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` z ) ) ` n ) = ( ( 1st ` ( 1st ` z ) ) ` n ) )
153 118 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { 0 } ) ` n ) = 0 )
154 153 adantl 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { 0 } ) ` n ) = 0 )
155 82 ffvelcdmda 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` z ) ) ` n ) e. ( 0 ..^ K ) )
156 elfzonn0 
 |-  ( ( ( 1st ` ( 1st ` z ) ) ` n ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` z ) ) ` n ) e. NN0 )
157 155 156 syl 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` z ) ) ` n ) e. NN0 )
158 157 nn0cnd 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` z ) ) ` n ) e. CC )
159 158 addridd 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` z ) ) ` n ) + 0 ) = ( ( 1st ` ( 1st ` z ) ) ` n ) )
160 148 149 151 149 152 154 159 offveq 
 |-  ( z e. S -> ( ( 1st ` ( 1st ` z ) ) oF + ( ( 1 ... N ) X. { 0 } ) ) = ( 1st ` ( 1st ` z ) ) )
161 147 160 eqtrd 
 |-  ( z e. S -> ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... N ) ) X. { 0 } ) ) = ( 1st ` ( 1st ` z ) ) )
162 141 161 eqtrid 
 |-  ( z e. S -> [_ 0 / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( 1st ` ( 1st ` z ) ) )
163 162 ad2antlr 
 |-  ( ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ y = 0 ) -> [_ 0 / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( 1st ` ( 1st ` z ) ) )
164 117 163 eqtrd 
 |-  ( ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ y = 0 ) -> [_ if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` z ) ) oF + ( ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( 1st ` ( 1st ` z ) ) )
165 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
166 1 165 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
167 0elfz 
 |-  ( ( N - 1 ) e. NN0 -> 0 e. ( 0 ... ( N - 1 ) ) )
168 166 167 syl 
 |-  ( ph -> 0 e. ( 0 ... ( N - 1 ) ) )
169 168 ad2antrr 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> 0 e. ( 0 ... ( N - 1 ) ) )
170 fvexd 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( 1st ` ( 1st ` z ) ) e. _V )
171 108 164 169 170 fvmptd 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( F ` 0 ) = ( 1st ` ( 1st ` z ) ) )
172 107 171 sylan 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) /\ z e. S ) -> ( F ` 0 ) = ( 1st ` ( 1st ` z ) ) )
173 172 an32s 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) -> ( F ` 0 ) = ( 1st ` ( 1st ` z ) ) )
174 103 173 mpdan 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( F ` 0 ) = ( 1st ` ( 1st ` z ) ) )
175 fveq2 
 |-  ( z = T -> ( 2nd ` z ) = ( 2nd ` T ) )
176 175 eleq1d 
 |-  ( z = T -> ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) <-> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) )
177 176 anbi2d 
 |-  ( z = T -> ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) <-> ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) ) )
178 2fveq3 
 |-  ( z = T -> ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) )
179 178 eqeq2d 
 |-  ( z = T -> ( ( F ` 0 ) = ( 1st ` ( 1st ` z ) ) <-> ( F ` 0 ) = ( 1st ` ( 1st ` T ) ) ) )
180 177 179 imbi12d 
 |-  ( z = T -> ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( F ` 0 ) = ( 1st ` ( 1st ` z ) ) ) <-> ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( F ` 0 ) = ( 1st ` ( 1st ` T ) ) ) ) )
181 171 expcom 
 |-  ( z e. S -> ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( F ` 0 ) = ( 1st ` ( 1st ` z ) ) ) )
182 180 181 vtoclga 
 |-  ( T e. S -> ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( F ` 0 ) = ( 1st ` ( 1st ` T ) ) ) )
183 9 182 mpcom 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( F ` 0 ) = ( 1st ` ( 1st ` T ) ) )
184 183 adantr 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( F ` 0 ) = ( 1st ` ( 1st ` T ) ) )
185 174 184 eqtr3d 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) )
186 185 adantr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) )
187 1 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> N e. NN )
188 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> T e. S )
189 simpllr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
190 simplr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> z e. S )
191 36 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
192 xpopth 
 |-  ( ( ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` T ) ) ) <-> ( 1st ` z ) = ( 1st ` T ) ) )
193 78 191 192 syl2anr 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` T ) ) ) <-> ( 1st ` z ) = ( 1st ` T ) ) )
194 34 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
195 xpopth 
 |-  ( ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( ( 1st ` z ) = ( 1st ` T ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) <-> z = T ) )
196 195 biimpd 
 |-  ( ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( ( 1st ` z ) = ( 1st ` T ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) -> z = T ) )
197 76 194 196 syl2anr 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( ( ( 1st ` z ) = ( 1st ` T ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) -> z = T ) )
198 103 197 mpan2d 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( ( 1st ` z ) = ( 1st ` T ) -> z = T ) )
199 193 198 sylbid 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` T ) ) ) -> z = T ) )
200 185 199 mpand 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` T ) ) -> z = T ) )
201 200 necon3d 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( z =/= T -> ( 2nd ` ( 1st ` z ) ) =/= ( 2nd ` ( 1st ` T ) ) ) )
202 201 imp 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> ( 2nd ` ( 1st ` z ) ) =/= ( 2nd ` ( 1st ` T ) ) )
203 187 2 188 189 190 202 poimirlem9 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) )
204 103 adantr 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> ( 2nd ` z ) = ( 2nd ` T ) )
205 186 203 204 jca31 
 |-  ( ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) /\ z =/= T ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) )
206 205 ex 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( z =/= T -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) ) )
207 simplr 
 |-  ( ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) -> ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) )
208 elfznn 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) e. NN )
209 208 nnred 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) e. RR )
210 209 ltp1d 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) < ( ( 2nd ` T ) + 1 ) )
211 209 210 ltned 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) )
212 211 adantl 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) )
213 fveq1 
 |-  ( ( 2nd ` ( 1st ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ` ( 2nd ` T ) ) )
214 id 
 |-  ( ( 2nd ` T ) e. RR -> ( 2nd ` T ) e. RR )
215 ltp1 
 |-  ( ( 2nd ` T ) e. RR -> ( 2nd ` T ) < ( ( 2nd ` T ) + 1 ) )
216 214 215 ltned 
 |-  ( ( 2nd ` T ) e. RR -> ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) )
217 fvex 
 |-  ( 2nd ` T ) e. _V
218 ovex 
 |-  ( ( 2nd ` T ) + 1 ) e. _V
219 217 218 218 217 fpr 
 |-  ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
220 216 219 syl 
 |-  ( ( 2nd ` T ) e. RR -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
221 f1oi 
 |-  ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -1-1-onto-> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
222 f1of 
 |-  ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -1-1-onto-> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) --> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
223 221 222 ax-mp 
 |-  ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) --> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
224 disjdif 
 |-  ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = (/)
225 fun 
 |-  ( ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } /\ ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) --> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) /\ ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = (/) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) --> ( { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
226 224 225 mpan2 
 |-  ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } /\ ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) --> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) --> ( { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
227 220 223 226 sylancl 
 |-  ( ( 2nd ` T ) e. RR -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) --> ( { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
228 217 prid1 
 |-  ( 2nd ` T ) e. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) }
229 elun1 
 |-  ( ( 2nd ` T ) e. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -> ( 2nd ` T ) e. ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
230 228 229 ax-mp 
 |-  ( 2nd ` T ) e. ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
231 fvco3 
 |-  ( ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) --> ( { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) /\ ( 2nd ` T ) e. ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ` ( 2nd ` T ) ) ) )
232 227 230 231 sylancl 
 |-  ( ( 2nd ` T ) e. RR -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ` ( 2nd ` T ) ) ) )
233 220 ffnd 
 |-  ( ( 2nd ` T ) e. RR -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
234 fnresi 
 |-  ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) Fn ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
235 224 228 pm3.2i 
 |-  ( ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = (/) /\ ( 2nd ` T ) e. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
236 fvun1 
 |-  ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } /\ ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) Fn ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) /\ ( ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = (/) /\ ( 2nd ` T ) e. { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ` ( 2nd ` T ) ) = ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ` ( 2nd ` T ) ) )
237 234 235 236 mp3an23 
 |-  ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ` ( 2nd ` T ) ) = ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ` ( 2nd ` T ) ) )
238 233 237 syl 
 |-  ( ( 2nd ` T ) e. RR -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ` ( 2nd ` T ) ) = ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ` ( 2nd ` T ) ) )
239 217 218 fvpr1 
 |-  ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ` ( 2nd ` T ) ) = ( ( 2nd ` T ) + 1 ) )
240 216 239 syl 
 |-  ( ( 2nd ` T ) e. RR -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ` ( 2nd ` T ) ) = ( ( 2nd ` T ) + 1 ) )
241 238 240 eqtrd 
 |-  ( ( 2nd ` T ) e. RR -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` T ) + 1 ) )
242 241 fveq2d 
 |-  ( ( 2nd ` T ) e. RR -> ( ( 2nd ` ( 1st ` T ) ) ` ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ` ( 2nd ` T ) ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) )
243 232 242 eqtrd 
 |-  ( ( 2nd ` T ) e. RR -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) )
244 209 243 syl 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) )
245 244 eqeq2d 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ` ( 2nd ` T ) ) <-> ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) ) )
246 245 adantl 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ` ( 2nd ` T ) ) <-> ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) ) )
247 f1of1 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) )
248 51 247 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) )
249 248 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) )
250 1 nncnd 
 |-  ( ph -> N e. CC )
251 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
252 250 251 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
253 166 nn0zd 
 |-  ( ph -> ( N - 1 ) e. ZZ )
254 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
255 253 254 syl 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
256 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
257 255 256 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
258 252 257 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
259 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
260 258 259 syl 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
261 260 sselda 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` T ) e. ( 1 ... N ) )
262 fzp1elp1 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
263 262 adantl 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
264 252 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
265 264 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
266 263 265 eleqtrd 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) )
267 f1veqaeq 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) /\ ( ( 2nd ` T ) e. ( 1 ... N ) /\ ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) -> ( 2nd ` T ) = ( ( 2nd ` T ) + 1 ) ) )
268 249 261 266 267 syl12anc 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) -> ( 2nd ` T ) = ( ( 2nd ` T ) + 1 ) ) )
269 246 268 sylbid 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ` ( 2nd ` T ) ) -> ( 2nd ` T ) = ( ( 2nd ` T ) + 1 ) ) )
270 213 269 syl5 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> ( 2nd ` T ) = ( ( 2nd ` T ) + 1 ) ) )
271 270 necon3d 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) -> ( 2nd ` ( 1st ` T ) ) =/= ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) )
272 212 271 mpd 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` ( 1st ` T ) ) =/= ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) )
273 2fveq3 
 |-  ( z = T -> ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` T ) ) )
274 273 neeq1d 
 |-  ( z = T -> ( ( 2nd ` ( 1st ` z ) ) =/= ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) <-> ( 2nd ` ( 1st ` T ) ) =/= ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) )
275 272 274 syl5ibrcom 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( z = T -> ( 2nd ` ( 1st ` z ) ) =/= ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) )
276 275 necon2d 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> z =/= T ) )
277 207 276 syl5 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) -> z =/= T ) )
278 277 adantr 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) -> z =/= T ) )
279 206 278 impbid 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( z =/= T <-> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) ) )
280 eqop 
 |-  ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( z = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. <-> ( ( 1st ` z ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. /\ ( 2nd ` z ) = ( 2nd ` T ) ) ) )
281 eqop 
 |-  ( ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( ( 1st ` z ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. <-> ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) ) )
282 77 281 syl 
 |-  ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( ( 1st ` z ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. <-> ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) ) )
283 282 anbi1d 
 |-  ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( ( ( 1st ` z ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. /\ ( 2nd ` z ) = ( 2nd ` T ) ) <-> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) ) )
284 280 283 bitrd 
 |-  ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( z = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. <-> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) ) )
285 76 284 syl 
 |-  ( z e. S -> ( z = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. <-> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) ) )
286 285 adantl 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( z = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. <-> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) /\ ( 2nd ` z ) = ( 2nd ` T ) ) ) )
287 279 286 bitr4d 
 |-  ( ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) /\ z e. S ) -> ( z =/= T <-> z = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. ) )
288 287 ralrimiva 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> A. z e. S ( z =/= T <-> z = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. ) )
289 reu6i 
 |-  ( ( <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. e. S /\ A. z e. S ( z =/= T <-> z = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. ) ) -> E! z e. S z =/= T )
290 11 288 289 syl2anc 
 |-  ( ( ph /\ ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> E! z e. S z =/= T )
291 xp2nd 
 |-  ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 2nd ` T ) e. ( 0 ... N ) )
292 34 291 syl 
 |-  ( ph -> ( 2nd ` T ) e. ( 0 ... N ) )
293 292 biantrurd 
 |-  ( ph -> ( -. ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) <-> ( ( 2nd ` T ) e. ( 0 ... N ) /\ -. ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) ) )
294 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
295 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
296 294 295 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
297 fzpred 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( 0 ... N ) = ( { 0 } u. ( ( 0 + 1 ) ... N ) ) )
298 296 297 syl 
 |-  ( ph -> ( 0 ... N ) = ( { 0 } u. ( ( 0 + 1 ) ... N ) ) )
299 125 oveq1i 
 |-  ( ( 0 + 1 ) ... N ) = ( 1 ... N )
300 299 uneq2i 
 |-  ( { 0 } u. ( ( 0 + 1 ) ... N ) ) = ( { 0 } u. ( 1 ... N ) )
301 298 300 eqtrdi 
 |-  ( ph -> ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) ) )
302 301 difeq1d 
 |-  ( ph -> ( ( 0 ... N ) \ ( 1 ... ( N - 1 ) ) ) = ( ( { 0 } u. ( 1 ... N ) ) \ ( 1 ... ( N - 1 ) ) ) )
303 difundir 
 |-  ( ( { 0 } u. ( 1 ... N ) ) \ ( 1 ... ( N - 1 ) ) ) = ( ( { 0 } \ ( 1 ... ( N - 1 ) ) ) u. ( ( 1 ... N ) \ ( 1 ... ( N - 1 ) ) ) )
304 0lt1 
 |-  0 < 1
305 0re 
 |-  0 e. RR
306 1re 
 |-  1 e. RR
307 305 306 ltnlei 
 |-  ( 0 < 1 <-> -. 1 <_ 0 )
308 304 307 mpbi 
 |-  -. 1 <_ 0
309 elfzle1 
 |-  ( 0 e. ( 1 ... ( N - 1 ) ) -> 1 <_ 0 )
310 308 309 mto 
 |-  -. 0 e. ( 1 ... ( N - 1 ) )
311 incom 
 |-  ( ( 1 ... ( N - 1 ) ) i^i { 0 } ) = ( { 0 } i^i ( 1 ... ( N - 1 ) ) )
312 311 eqeq1i 
 |-  ( ( ( 1 ... ( N - 1 ) ) i^i { 0 } ) = (/) <-> ( { 0 } i^i ( 1 ... ( N - 1 ) ) ) = (/) )
313 disjsn 
 |-  ( ( ( 1 ... ( N - 1 ) ) i^i { 0 } ) = (/) <-> -. 0 e. ( 1 ... ( N - 1 ) ) )
314 disj3 
 |-  ( ( { 0 } i^i ( 1 ... ( N - 1 ) ) ) = (/) <-> { 0 } = ( { 0 } \ ( 1 ... ( N - 1 ) ) ) )
315 312 313 314 3bitr3i 
 |-  ( -. 0 e. ( 1 ... ( N - 1 ) ) <-> { 0 } = ( { 0 } \ ( 1 ... ( N - 1 ) ) ) )
316 310 315 mpbi 
 |-  { 0 } = ( { 0 } \ ( 1 ... ( N - 1 ) ) )
317 316 uneq1i 
 |-  ( { 0 } u. ( ( 1 ... N ) \ ( 1 ... ( N - 1 ) ) ) ) = ( ( { 0 } \ ( 1 ... ( N - 1 ) ) ) u. ( ( 1 ... N ) \ ( 1 ... ( N - 1 ) ) ) )
318 303 317 eqtr4i 
 |-  ( ( { 0 } u. ( 1 ... N ) ) \ ( 1 ... ( N - 1 ) ) ) = ( { 0 } u. ( ( 1 ... N ) \ ( 1 ... ( N - 1 ) ) ) )
319 difundir 
 |-  ( ( ( 1 ... ( N - 1 ) ) u. { N } ) \ ( 1 ... ( N - 1 ) ) ) = ( ( ( 1 ... ( N - 1 ) ) \ ( 1 ... ( N - 1 ) ) ) u. ( { N } \ ( 1 ... ( N - 1 ) ) ) )
320 difid 
 |-  ( ( 1 ... ( N - 1 ) ) \ ( 1 ... ( N - 1 ) ) ) = (/)
321 320 uneq1i 
 |-  ( ( ( 1 ... ( N - 1 ) ) \ ( 1 ... ( N - 1 ) ) ) u. ( { N } \ ( 1 ... ( N - 1 ) ) ) ) = ( (/) u. ( { N } \ ( 1 ... ( N - 1 ) ) ) )
322 uncom 
 |-  ( (/) u. ( { N } \ ( 1 ... ( N - 1 ) ) ) ) = ( ( { N } \ ( 1 ... ( N - 1 ) ) ) u. (/) )
323 un0 
 |-  ( ( { N } \ ( 1 ... ( N - 1 ) ) ) u. (/) ) = ( { N } \ ( 1 ... ( N - 1 ) ) )
324 322 323 eqtri 
 |-  ( (/) u. ( { N } \ ( 1 ... ( N - 1 ) ) ) ) = ( { N } \ ( 1 ... ( N - 1 ) ) )
325 319 321 324 3eqtri 
 |-  ( ( ( 1 ... ( N - 1 ) ) u. { N } ) \ ( 1 ... ( N - 1 ) ) ) = ( { N } \ ( 1 ... ( N - 1 ) ) )
326 nnuz 
 |-  NN = ( ZZ>= ` 1 )
327 1 326 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
328 252 327 eqeltrd 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
329 fzsplit2 
 |-  ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
330 328 258 329 syl2anc 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
331 252 oveq1d 
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
332 1 nnzd 
 |-  ( ph -> N e. ZZ )
333 fzsn 
 |-  ( N e. ZZ -> ( N ... N ) = { N } )
334 332 333 syl 
 |-  ( ph -> ( N ... N ) = { N } )
335 331 334 eqtrd 
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
336 335 uneq2d 
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
337 330 336 eqtrd 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
338 337 difeq1d 
 |-  ( ph -> ( ( 1 ... N ) \ ( 1 ... ( N - 1 ) ) ) = ( ( ( 1 ... ( N - 1 ) ) u. { N } ) \ ( 1 ... ( N - 1 ) ) ) )
339 1 nnred 
 |-  ( ph -> N e. RR )
340 339 ltm1d 
 |-  ( ph -> ( N - 1 ) < N )
341 166 nn0red 
 |-  ( ph -> ( N - 1 ) e. RR )
342 341 339 ltnled 
 |-  ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
343 340 342 mpbid 
 |-  ( ph -> -. N <_ ( N - 1 ) )
344 elfzle2 
 |-  ( N e. ( 1 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
345 343 344 nsyl 
 |-  ( ph -> -. N e. ( 1 ... ( N - 1 ) ) )
346 incom 
 |-  ( ( 1 ... ( N - 1 ) ) i^i { N } ) = ( { N } i^i ( 1 ... ( N - 1 ) ) )
347 346 eqeq1i 
 |-  ( ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) <-> ( { N } i^i ( 1 ... ( N - 1 ) ) ) = (/) )
348 disjsn 
 |-  ( ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) <-> -. N e. ( 1 ... ( N - 1 ) ) )
349 disj3 
 |-  ( ( { N } i^i ( 1 ... ( N - 1 ) ) ) = (/) <-> { N } = ( { N } \ ( 1 ... ( N - 1 ) ) ) )
350 347 348 349 3bitr3i 
 |-  ( -. N e. ( 1 ... ( N - 1 ) ) <-> { N } = ( { N } \ ( 1 ... ( N - 1 ) ) ) )
351 345 350 sylib 
 |-  ( ph -> { N } = ( { N } \ ( 1 ... ( N - 1 ) ) ) )
352 325 338 351 3eqtr4a 
 |-  ( ph -> ( ( 1 ... N ) \ ( 1 ... ( N - 1 ) ) ) = { N } )
353 352 uneq2d 
 |-  ( ph -> ( { 0 } u. ( ( 1 ... N ) \ ( 1 ... ( N - 1 ) ) ) ) = ( { 0 } u. { N } ) )
354 318 353 eqtrid 
 |-  ( ph -> ( ( { 0 } u. ( 1 ... N ) ) \ ( 1 ... ( N - 1 ) ) ) = ( { 0 } u. { N } ) )
355 302 354 eqtrd 
 |-  ( ph -> ( ( 0 ... N ) \ ( 1 ... ( N - 1 ) ) ) = ( { 0 } u. { N } ) )
356 355 eleq2d 
 |-  ( ph -> ( ( 2nd ` T ) e. ( ( 0 ... N ) \ ( 1 ... ( N - 1 ) ) ) <-> ( 2nd ` T ) e. ( { 0 } u. { N } ) ) )
357 eldif 
 |-  ( ( 2nd ` T ) e. ( ( 0 ... N ) \ ( 1 ... ( N - 1 ) ) ) <-> ( ( 2nd ` T ) e. ( 0 ... N ) /\ -. ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) )
358 elun 
 |-  ( ( 2nd ` T ) e. ( { 0 } u. { N } ) <-> ( ( 2nd ` T ) e. { 0 } \/ ( 2nd ` T ) e. { N } ) )
359 217 elsn 
 |-  ( ( 2nd ` T ) e. { 0 } <-> ( 2nd ` T ) = 0 )
360 217 elsn 
 |-  ( ( 2nd ` T ) e. { N } <-> ( 2nd ` T ) = N )
361 359 360 orbi12i 
 |-  ( ( ( 2nd ` T ) e. { 0 } \/ ( 2nd ` T ) e. { N } ) <-> ( ( 2nd ` T ) = 0 \/ ( 2nd ` T ) = N ) )
362 358 361 bitri 
 |-  ( ( 2nd ` T ) e. ( { 0 } u. { N } ) <-> ( ( 2nd ` T ) = 0 \/ ( 2nd ` T ) = N ) )
363 356 357 362 3bitr3g 
 |-  ( ph -> ( ( ( 2nd ` T ) e. ( 0 ... N ) /\ -. ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) <-> ( ( 2nd ` T ) = 0 \/ ( 2nd ` T ) = N ) ) )
364 293 363 bitrd 
 |-  ( ph -> ( -. ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) <-> ( ( 2nd ` T ) = 0 \/ ( 2nd ` T ) = N ) ) )
365 364 biimpa 
 |-  ( ( ph /\ -. ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) = 0 \/ ( 2nd ` T ) = N ) )
366 1 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) = 0 ) -> N e. NN )
367 3 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) = 0 ) -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
368 4 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) = 0 ) -> T e. S )
369 6 adantlr 
 |-  ( ( ( ph /\ ( 2nd ` T ) = 0 ) /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= K )
370 simpr 
 |-  ( ( ph /\ ( 2nd ` T ) = 0 ) -> ( 2nd ` T ) = 0 )
371 366 2 367 368 369 370 poimirlem18 
 |-  ( ( ph /\ ( 2nd ` T ) = 0 ) -> E! z e. S z =/= T )
372 1 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) = N ) -> N e. NN )
373 3 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) = N ) -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
374 4 adantr 
 |-  ( ( ph /\ ( 2nd ` T ) = N ) -> T e. S )
375 5 adantlr 
 |-  ( ( ( ph /\ ( 2nd ` T ) = N ) /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= 0 )
376 simpr 
 |-  ( ( ph /\ ( 2nd ` T ) = N ) -> ( 2nd ` T ) = N )
377 372 2 373 374 375 376 poimirlem21 
 |-  ( ( ph /\ ( 2nd ` T ) = N ) -> E! z e. S z =/= T )
378 371 377 jaodan 
 |-  ( ( ph /\ ( ( 2nd ` T ) = 0 \/ ( 2nd ` T ) = N ) ) -> E! z e. S z =/= T )
379 365 378 syldan 
 |-  ( ( ph /\ -. ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) ) -> E! z e. S z =/= T )
380 290 379 pm2.61dan 
 |-  ( ph -> E! z e. S z =/= T )