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