Metamath Proof Explorer

Theorem poimirlem18

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