Metamath Proof Explorer

Theorem poimirlem21

Description: Lemma for poimir stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (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 )
poimirlem21.4 
|- ( ph -> ( 2nd ` T ) = N )
Assertion poimirlem21 
|- ( 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 poimirlem21.4 
 |-  ( ph -> ( 2nd ` T ) = N )
7 1 2 3 4 5 6 poimirlem20 
 |-  ( ph -> E. z e. S z =/= T )
8 6 adantr 
 |-  ( ( ph /\ z e. S ) -> ( 2nd ` T ) = N )
9 1 nnred 
 |-  ( ph -> N e. RR )
10 9 ltm1d 
 |-  ( ph -> ( N - 1 ) < N )
11 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
12 1 11 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
13 12 nn0red 
 |-  ( ph -> ( N - 1 ) e. RR )
14 13 9 ltnled 
 |-  ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
15 10 14 mpbid 
 |-  ( ph -> -. N <_ ( N - 1 ) )
16 elfzle2 
 |-  ( N e. ( 1 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
17 15 16 nsyl 
 |-  ( ph -> -. N e. ( 1 ... ( N - 1 ) ) )
18 eleq1 
 |-  ( ( 2nd ` z ) = N -> ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) <-> N e. ( 1 ... ( N - 1 ) ) ) )
19 18 notbid 
 |-  ( ( 2nd ` z ) = N -> ( -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) <-> -. N e. ( 1 ... ( N - 1 ) ) ) )
20 17 19 syl5ibrcom 
 |-  ( ph -> ( ( 2nd ` z ) = N -> -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
21 20 necon2ad 
 |-  ( ph -> ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` z ) =/= N ) )
22 21 adantr 
 |-  ( ( ph /\ z e. S ) -> ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` z ) =/= N ) )
23 1 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> N e. NN )
24 fveq2 
 |-  ( t = z -> ( 2nd ` t ) = ( 2nd ` z ) )
25 24 breq2d 
 |-  ( t = z -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` z ) ) )
26 25 ifbid 
 |-  ( t = z -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` z ) , y , ( y + 1 ) ) )
27 26 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 } ) ) ) )
28 2fveq3 
 |-  ( t = z -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` z ) ) )
29 2fveq3 
 |-  ( t = z -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` z ) ) )
30 29 imaeq1d 
 |-  ( t = z -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) )
31 30 xpeq1d 
 |-  ( t = z -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... j ) ) X. { 1 } ) )
32 29 imaeq1d 
 |-  ( t = z -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) )
33 32 xpeq1d 
 |-  ( t = z -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
34 31 33 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 } ) ) )
35 28 34 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 } ) ) ) )
36 35 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 } ) ) ) )
37 27 36 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 } ) ) ) )
38 37 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 } ) ) ) ) )
39 38 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 } ) ) ) ) ) )
40 39 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 } ) ) ) ) ) )
41 40 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 } ) ) ) ) )
42 41 ad2antlr 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> 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 } ) ) ) ) )
43 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 ) ) )
44 43 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 ) ) )
45 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 ) } ) )
46 44 45 syl 
 |-  ( z e. S -> ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
47 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 ) ) )
48 46 47 syl 
 |-  ( z e. S -> ( 1st ` ( 1st ` z ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
49 elmapi 
 |-  ( ( 1st ` ( 1st ` z ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
50 48 49 syl 
 |-  ( z e. S -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
51 elfzoelz 
 |-  ( n e. ( 0 ..^ K ) -> n e. ZZ )
52 51 ssriv 
 |-  ( 0 ..^ K ) C_ ZZ
53 fss 
 |-  ( ( ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ( 0 ..^ K ) /\ ( 0 ..^ K ) C_ ZZ ) -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ZZ )
54 50 52 53 sylancl 
 |-  ( z e. S -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ZZ )
55 54 ad2antlr 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( 1st ` ( 1st ` z ) ) : ( 1 ... N ) --> ZZ )
56 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 ) } )
57 46 56 syl 
 |-  ( z e. S -> ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
58 fvex 
 |-  ( 2nd ` ( 1st ` z ) ) e. _V
59 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` z ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
60 58 59 elab 
 |-  ( ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
61 57 60 sylib 
 |-  ( z e. S -> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
62 61 ad2antlr 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
63 simpr 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) )
64 23 42 55 62 63 poimirlem1 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> -. E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` z ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` z ) ) ` n ) )
65 1 ad2antrr 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) =/= ( 2nd ` z ) ) -> N e. NN )
66 fveq2 
 |-  ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
67 66 breq2d 
 |-  ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
68 67 ifbid 
 |-  ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
69 68 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 } ) ) ) )
70 2fveq3 
 |-  ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
71 2fveq3 
 |-  ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
72 71 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
73 72 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
74 71 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
75 74 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
76 73 75 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 } ) ) )
77 70 76 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 } ) ) ) )
78 77 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 } ) ) ) )
79 69 78 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 } ) ) ) )
80 79 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 } ) ) ) ) )
81 80 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 } ) ) ) ) ) )
82 81 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 } ) ) ) ) ) )
83 82 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 } ) ) ) ) )
84 4 83 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 } ) ) ) ) )
85 84 ad2antrr 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) =/= ( 2nd ` 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 } ) ) ) ) )
86 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 ) ) )
87 86 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 ) ) )
88 4 87 syl 
 |-  ( ph -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
89 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 ) } ) )
90 88 89 syl 
 |-  ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
91 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 ) ) )
92 90 91 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
93 elmapi 
 |-  ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
94 92 93 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
95 fss 
 |-  ( ( ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) /\ ( 0 ..^ K ) C_ ZZ ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ZZ )
96 94 52 95 sylancl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ZZ )
97 96 ad2antrr 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) =/= ( 2nd ` z ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ZZ )
98 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 ) } )
99 90 98 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
100 fvex 
 |-  ( 2nd ` ( 1st ` T ) ) e. _V
101 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
102 100 101 elab 
 |-  ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
103 99 102 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
104 103 ad2antrr 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) =/= ( 2nd ` z ) ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
105 simplr 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) =/= ( 2nd ` z ) ) -> ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) )
106 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 ) )
107 88 106 syl 
 |-  ( ph -> ( 2nd ` T ) e. ( 0 ... N ) )
108 107 adantr 
 |-  ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` T ) e. ( 0 ... N ) )
109 eldifsn 
 |-  ( ( 2nd ` T ) e. ( ( 0 ... N ) \ { ( 2nd ` z ) } ) <-> ( ( 2nd ` T ) e. ( 0 ... N ) /\ ( 2nd ` T ) =/= ( 2nd ` z ) ) )
110 109 biimpri 
 |-  ( ( ( 2nd ` T ) e. ( 0 ... N ) /\ ( 2nd ` T ) =/= ( 2nd ` z ) ) -> ( 2nd ` T ) e. ( ( 0 ... N ) \ { ( 2nd ` z ) } ) )
111 108 110 sylan 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) =/= ( 2nd ` z ) ) -> ( 2nd ` T ) e. ( ( 0 ... N ) \ { ( 2nd ` z ) } ) )
112 65 85 97 104 105 111 poimirlem2 
 |-  ( ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) =/= ( 2nd ` z ) ) -> E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` z ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` z ) ) ` n ) )
113 112 ex 
 |-  ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) =/= ( 2nd ` z ) -> E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` z ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` z ) ) ` n ) ) )
114 113 necon1bd 
 |-  ( ( ph /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( -. E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` z ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` z ) ) ` n ) -> ( 2nd ` T ) = ( 2nd ` z ) ) )
115 114 adantlr 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( -. E* n e. ( 1 ... N ) ( ( F ` ( ( 2nd ` z ) - 1 ) ) ` n ) =/= ( ( F ` ( 2nd ` z ) ) ` n ) -> ( 2nd ` T ) = ( 2nd ` z ) ) )
116 64 115 mpd 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` T ) = ( 2nd ` z ) )
117 116 neeq1d 
 |-  ( ( ( ph /\ z e. S ) /\ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) =/= N <-> ( 2nd ` z ) =/= N ) )
118 117 exbiri 
 |-  ( ( ph /\ z e. S ) -> ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) -> ( ( 2nd ` z ) =/= N -> ( 2nd ` T ) =/= N ) ) )
119 22 118 mpdd 
 |-  ( ( ph /\ z e. S ) -> ( ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) =/= N ) )
120 119 necon2bd 
 |-  ( ( ph /\ z e. S ) -> ( ( 2nd ` T ) = N -> -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
121 8 120 mpd 
 |-  ( ( ph /\ z e. S ) -> -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) )
122 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 ) )
123 44 122 syl 
 |-  ( z e. S -> ( 2nd ` z ) e. ( 0 ... N ) )
124 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
125 12 124 eleqtrdi 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
126 fzpred 
 |-  ( ( N - 1 ) e. ( ZZ>= ` 0 ) -> ( 0 ... ( N - 1 ) ) = ( { 0 } u. ( ( 0 + 1 ) ... ( N - 1 ) ) ) )
127 125 126 syl 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) = ( { 0 } u. ( ( 0 + 1 ) ... ( N - 1 ) ) ) )
128 0p1e1 
 |-  ( 0 + 1 ) = 1
129 128 oveq1i 
 |-  ( ( 0 + 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) )
130 129 uneq2i 
 |-  ( { 0 } u. ( ( 0 + 1 ) ... ( N - 1 ) ) ) = ( { 0 } u. ( 1 ... ( N - 1 ) ) )
131 127 130 eqtrdi 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) = ( { 0 } u. ( 1 ... ( N - 1 ) ) ) )
132 131 eleq2d 
 |-  ( ph -> ( ( 2nd ` z ) e. ( 0 ... ( N - 1 ) ) <-> ( 2nd ` z ) e. ( { 0 } u. ( 1 ... ( N - 1 ) ) ) ) )
133 132 notbid 
 |-  ( ph -> ( -. ( 2nd ` z ) e. ( 0 ... ( N - 1 ) ) <-> -. ( 2nd ` z ) e. ( { 0 } u. ( 1 ... ( N - 1 ) ) ) ) )
134 ioran 
 |-  ( -. ( ( 2nd ` z ) = 0 \/ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) <-> ( -. ( 2nd ` z ) = 0 /\ -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
135 elun 
 |-  ( ( 2nd ` z ) e. ( { 0 } u. ( 1 ... ( N - 1 ) ) ) <-> ( ( 2nd ` z ) e. { 0 } \/ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
136 fvex 
 |-  ( 2nd ` z ) e. _V
137 136 elsn 
 |-  ( ( 2nd ` z ) e. { 0 } <-> ( 2nd ` z ) = 0 )
138 137 orbi1i 
 |-  ( ( ( 2nd ` z ) e. { 0 } \/ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) <-> ( ( 2nd ` z ) = 0 \/ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
139 135 138 bitri 
 |-  ( ( 2nd ` z ) e. ( { 0 } u. ( 1 ... ( N - 1 ) ) ) <-> ( ( 2nd ` z ) = 0 \/ ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
140 134 139 xchnxbir 
 |-  ( -. ( 2nd ` z ) e. ( { 0 } u. ( 1 ... ( N - 1 ) ) ) <-> ( -. ( 2nd ` z ) = 0 /\ -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) )
141 133 140 bitrdi 
 |-  ( ph -> ( -. ( 2nd ` z ) e. ( 0 ... ( N - 1 ) ) <-> ( -. ( 2nd ` z ) = 0 /\ -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) ) )
142 141 anbi2d 
 |-  ( ph -> ( ( ( 2nd ` z ) e. ( 0 ... N ) /\ -. ( 2nd ` z ) e. ( 0 ... ( N - 1 ) ) ) <-> ( ( 2nd ` z ) e. ( 0 ... N ) /\ ( -. ( 2nd ` z ) = 0 /\ -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) ) ) )
143 uncom 
 |-  ( ( 0 ... ( N - 1 ) ) u. { N } ) = ( { N } u. ( 0 ... ( N - 1 ) ) )
144 143 difeq1i 
 |-  ( ( ( 0 ... ( N - 1 ) ) u. { N } ) \ ( 0 ... ( N - 1 ) ) ) = ( ( { N } u. ( 0 ... ( N - 1 ) ) ) \ ( 0 ... ( N - 1 ) ) )
145 difun2 
 |-  ( ( { N } u. ( 0 ... ( N - 1 ) ) ) \ ( 0 ... ( N - 1 ) ) ) = ( { N } \ ( 0 ... ( N - 1 ) ) )
146 144 145 eqtri 
 |-  ( ( ( 0 ... ( N - 1 ) ) u. { N } ) \ ( 0 ... ( N - 1 ) ) ) = ( { N } \ ( 0 ... ( N - 1 ) ) )
147 1 nncnd 
 |-  ( ph -> N e. CC )
148 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
149 147 148 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
150 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
151 150 124 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
152 149 151 eqeltrd 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 0 ) )
153 12 nn0zd 
 |-  ( ph -> ( N - 1 ) e. ZZ )
154 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
155 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
156 153 154 155 3syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
157 149 156 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
158 fzsplit2 
 |-  ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 0 ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
159 152 157 158 syl2anc 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
160 149 oveq1d 
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
161 1 nnzd 
 |-  ( ph -> N e. ZZ )
162 fzsn 
 |-  ( N e. ZZ -> ( N ... N ) = { N } )
163 161 162 syl 
 |-  ( ph -> ( N ... N ) = { N } )
164 160 163 eqtrd 
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
165 164 uneq2d 
 |-  ( ph -> ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( 0 ... ( N - 1 ) ) u. { N } ) )
166 159 165 eqtrd 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. { N } ) )
167 166 difeq1d 
 |-  ( ph -> ( ( 0 ... N ) \ ( 0 ... ( N - 1 ) ) ) = ( ( ( 0 ... ( N - 1 ) ) u. { N } ) \ ( 0 ... ( N - 1 ) ) ) )
168 elfzle2 
 |-  ( N e. ( 0 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
169 15 168 nsyl 
 |-  ( ph -> -. N e. ( 0 ... ( N - 1 ) ) )
170 incom 
 |-  ( ( 0 ... ( N - 1 ) ) i^i { N } ) = ( { N } i^i ( 0 ... ( N - 1 ) ) )
171 170 eqeq1i 
 |-  ( ( ( 0 ... ( N - 1 ) ) i^i { N } ) = (/) <-> ( { N } i^i ( 0 ... ( N - 1 ) ) ) = (/) )
172 disjsn 
 |-  ( ( ( 0 ... ( N - 1 ) ) i^i { N } ) = (/) <-> -. N e. ( 0 ... ( N - 1 ) ) )
173 disj3 
 |-  ( ( { N } i^i ( 0 ... ( N - 1 ) ) ) = (/) <-> { N } = ( { N } \ ( 0 ... ( N - 1 ) ) ) )
174 171 172 173 3bitr3i 
 |-  ( -. N e. ( 0 ... ( N - 1 ) ) <-> { N } = ( { N } \ ( 0 ... ( N - 1 ) ) ) )
175 169 174 sylib 
 |-  ( ph -> { N } = ( { N } \ ( 0 ... ( N - 1 ) ) ) )
176 146 167 175 3eqtr4a 
 |-  ( ph -> ( ( 0 ... N ) \ ( 0 ... ( N - 1 ) ) ) = { N } )
177 176 eleq2d 
 |-  ( ph -> ( ( 2nd ` z ) e. ( ( 0 ... N ) \ ( 0 ... ( N - 1 ) ) ) <-> ( 2nd ` z ) e. { N } ) )
178 eldif 
 |-  ( ( 2nd ` z ) e. ( ( 0 ... N ) \ ( 0 ... ( N - 1 ) ) ) <-> ( ( 2nd ` z ) e. ( 0 ... N ) /\ -. ( 2nd ` z ) e. ( 0 ... ( N - 1 ) ) ) )
179 136 elsn 
 |-  ( ( 2nd ` z ) e. { N } <-> ( 2nd ` z ) = N )
180 177 178 179 3bitr3g 
 |-  ( ph -> ( ( ( 2nd ` z ) e. ( 0 ... N ) /\ -. ( 2nd ` z ) e. ( 0 ... ( N - 1 ) ) ) <-> ( 2nd ` z ) = N ) )
181 142 180 bitr3d 
 |-  ( ph -> ( ( ( 2nd ` z ) e. ( 0 ... N ) /\ ( -. ( 2nd ` z ) = 0 /\ -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) ) <-> ( 2nd ` z ) = N ) )
182 181 biimpd 
 |-  ( ph -> ( ( ( 2nd ` z ) e. ( 0 ... N ) /\ ( -. ( 2nd ` z ) = 0 /\ -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) ) -> ( 2nd ` z ) = N ) )
183 182 expdimp 
 |-  ( ( ph /\ ( 2nd ` z ) e. ( 0 ... N ) ) -> ( ( -. ( 2nd ` z ) = 0 /\ -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` z ) = N ) )
184 123 183 sylan2 
 |-  ( ( ph /\ z e. S ) -> ( ( -. ( 2nd ` z ) = 0 /\ -. ( 2nd ` z ) e. ( 1 ... ( N - 1 ) ) ) -> ( 2nd ` z ) = N ) )
185 121 184 mpan2d 
 |-  ( ( ph /\ z e. S ) -> ( -. ( 2nd ` z ) = 0 -> ( 2nd ` z ) = N ) )
186 1 2 3 poimirlem14 
 |-  ( ph -> E* z e. S ( 2nd ` z ) = N )
187 fveqeq2 
 |-  ( z = s -> ( ( 2nd ` z ) = N <-> ( 2nd ` s ) = N ) )
188 187 rmo4 
 |-  ( E* z e. S ( 2nd ` z ) = N <-> A. z e. S A. s e. S ( ( ( 2nd ` z ) = N /\ ( 2nd ` s ) = N ) -> z = s ) )
189 186 188 sylib 
 |-  ( ph -> A. z e. S A. s e. S ( ( ( 2nd ` z ) = N /\ ( 2nd ` s ) = N ) -> z = s ) )
190 189 r19.21bi 
 |-  ( ( ph /\ z e. S ) -> A. s e. S ( ( ( 2nd ` z ) = N /\ ( 2nd ` s ) = N ) -> z = s ) )
191 4 adantr 
 |-  ( ( ph /\ z e. S ) -> T e. S )
192 fveqeq2 
 |-  ( s = T -> ( ( 2nd ` s ) = N <-> ( 2nd ` T ) = N ) )
193 192 anbi2d 
 |-  ( s = T -> ( ( ( 2nd ` z ) = N /\ ( 2nd ` s ) = N ) <-> ( ( 2nd ` z ) = N /\ ( 2nd ` T ) = N ) ) )
194 eqeq2 
 |-  ( s = T -> ( z = s <-> z = T ) )
195 193 194 imbi12d 
 |-  ( s = T -> ( ( ( ( 2nd ` z ) = N /\ ( 2nd ` s ) = N ) -> z = s ) <-> ( ( ( 2nd ` z ) = N /\ ( 2nd ` T ) = N ) -> z = T ) ) )
196 195 rspccv 
 |-  ( A. s e. S ( ( ( 2nd ` z ) = N /\ ( 2nd ` s ) = N ) -> z = s ) -> ( T e. S -> ( ( ( 2nd ` z ) = N /\ ( 2nd ` T ) = N ) -> z = T ) ) )
197 190 191 196 sylc 
 |-  ( ( ph /\ z e. S ) -> ( ( ( 2nd ` z ) = N /\ ( 2nd ` T ) = N ) -> z = T ) )
198 8 197 mpan2d 
 |-  ( ( ph /\ z e. S ) -> ( ( 2nd ` z ) = N -> z = T ) )
199 185 198 syld 
 |-  ( ( ph /\ z e. S ) -> ( -. ( 2nd ` z ) = 0 -> z = T ) )
200 199 necon1ad 
 |-  ( ( ph /\ z e. S ) -> ( z =/= T -> ( 2nd ` z ) = 0 ) )
201 200 ralrimiva 
 |-  ( ph -> A. z e. S ( z =/= T -> ( 2nd ` z ) = 0 ) )
202 1 2 3 poimirlem13 
 |-  ( ph -> E* z e. S ( 2nd ` z ) = 0 )
203 rmoim 
 |-  ( A. z e. S ( z =/= T -> ( 2nd ` z ) = 0 ) -> ( E* z e. S ( 2nd ` z ) = 0 -> E* z e. S z =/= T ) )
204 201 202 203 sylc 
 |-  ( ph -> E* z e. S z =/= T )
205 reu5 
 |-  ( E! z e. S z =/= T <-> ( E. z e. S z =/= T /\ E* z e. S z =/= T ) )
206 7 204 205 sylanbrc 
 |-  ( ph -> E! z e. S z =/= T )