Metamath Proof Explorer

Theorem poimirlem13

Description: Lemma for poimir - for at most one simplex associated with a shared face is the opposite vertex first on the walk. (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 ) ) )
Assertion poimirlem13 
|- ( ph -> E* z e. S ( 2nd ` z ) = 0 )

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 1 ad2antrr 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> N e. NN )
5 3 ad2antrr 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
6 simplrl 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> z e. S )
7 simprl 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` z ) = 0 )
8 4 2 5 6 7 poimirlem10 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( ( F ` ( N - 1 ) ) oF - ( ( 1 ... N ) X. { 1 } ) ) = ( 1st ` ( 1st ` z ) ) )
9 simplrr 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> k e. S )
10 simprr 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` k ) = 0 )
11 4 2 5 9 10 poimirlem10 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( ( F ` ( N - 1 ) ) oF - ( ( 1 ... N ) X. { 1 } ) ) = ( 1st ` ( 1st ` k ) ) )
12 8 11 eqtr3d 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` k ) ) )
13 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 ) ) )
14 13 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 ) ) )
15 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 ) } ) )
16 14 15 syl 
 |-  ( z e. S -> ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
17 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 ) } )
18 16 17 syl 
 |-  ( z e. S -> ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
19 fvex 
 |-  ( 2nd ` ( 1st ` z ) ) e. _V
20 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` z ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
21 19 20 elab 
 |-  ( ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
22 18 21 sylib 
 |-  ( z e. S -> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
23 f1ofn 
 |-  ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) )
24 22 23 syl 
 |-  ( z e. S -> ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) )
25 24 adantr 
 |-  ( ( z e. S /\ k e. S ) -> ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) )
26 25 ad2antlr 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) )
27 elrabi 
 |-  ( k 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 } ) ) ) ) } -> k e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
28 27 2 eleq2s 
 |-  ( k e. S -> k e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
29 xp1st 
 |-  ( k e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` k ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
30 28 29 syl 
 |-  ( k e. S -> ( 1st ` k ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
31 xp2nd 
 |-  ( ( 1st ` k ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
32 30 31 syl 
 |-  ( k e. S -> ( 2nd ` ( 1st ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
33 fvex 
 |-  ( 2nd ` ( 1st ` k ) ) e. _V
34 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` k ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
35 33 34 elab 
 |-  ( ( 2nd ` ( 1st ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
36 32 35 sylib 
 |-  ( k e. S -> ( 2nd ` ( 1st ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
37 f1ofn 
 |-  ( ( 2nd ` ( 1st ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` k ) ) Fn ( 1 ... N ) )
38 36 37 syl 
 |-  ( k e. S -> ( 2nd ` ( 1st ` k ) ) Fn ( 1 ... N ) )
39 38 adantl 
 |-  ( ( z e. S /\ k e. S ) -> ( 2nd ` ( 1st ` k ) ) Fn ( 1 ... N ) )
40 39 ad2antlr 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` ( 1st ` k ) ) Fn ( 1 ... N ) )
41 eleq1 
 |-  ( m = n -> ( m e. ( 1 ... N ) <-> n e. ( 1 ... N ) ) )
42 41 anbi2d 
 |-  ( m = n -> ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) <-> ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) ) )
43 oveq2 
 |-  ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
44 43 imaeq2d 
 |-  ( m = n -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) )
45 43 imaeq2d 
 |-  ( m = n -> ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) )
46 44 45 eqeq12d 
 |-  ( m = n -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) <-> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) ) )
47 42 46 imbi12d 
 |-  ( m = n -> ( ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) ) <-> ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) ) ) )
48 1 ad3antrrr 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> N e. NN )
49 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
50 simpl 
 |-  ( ( z e. S /\ k e. S ) -> z e. S )
51 50 ad3antlr 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> z e. S )
52 simplrl 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( 2nd ` z ) = 0 )
53 simpr 
 |-  ( ( z e. S /\ k e. S ) -> k e. S )
54 53 ad3antlr 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> k e. S )
55 simplrr 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( 2nd ` k ) = 0 )
56 simpr 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> m e. ( 1 ... N ) )
57 48 2 49 51 52 54 55 56 poimirlem11 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) C_ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) )
58 48 2 49 54 55 51 52 56 poimirlem11 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) C_ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) )
59 57 58 eqssd 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) )
60 47 59 chvarvv 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) )
61 simpll 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ph )
62 elfznn 
 |-  ( n e. ( 1 ... N ) -> n e. NN )
63 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
64 62 63 syl 
 |-  ( n e. ( 1 ... N ) -> ( n - 1 ) e. NN0 )
65 64 adantr 
 |-  ( ( n e. ( 1 ... N ) /\ -. n = 1 ) -> ( n - 1 ) e. NN0 )
66 62 nncnd 
 |-  ( n e. ( 1 ... N ) -> n e. CC )
67 ax-1cn 
 |-  1 e. CC
68 subeq0 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) = 0 <-> n = 1 ) )
69 66 67 68 sylancl 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = 0 <-> n = 1 ) )
70 69 necon3abid 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) =/= 0 <-> -. n = 1 ) )
71 70 biimpar 
 |-  ( ( n e. ( 1 ... N ) /\ -. n = 1 ) -> ( n - 1 ) =/= 0 )
72 elnnne0 
 |-  ( ( n - 1 ) e. NN <-> ( ( n - 1 ) e. NN0 /\ ( n - 1 ) =/= 0 ) )
73 65 71 72 sylanbrc 
 |-  ( ( n e. ( 1 ... N ) /\ -. n = 1 ) -> ( n - 1 ) e. NN )
74 73 adantl 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( n - 1 ) e. NN )
75 64 nn0red 
 |-  ( n e. ( 1 ... N ) -> ( n - 1 ) e. RR )
76 75 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n - 1 ) e. RR )
77 62 nnred 
 |-  ( n e. ( 1 ... N ) -> n e. RR )
78 77 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n e. RR )
79 1 nnred 
 |-  ( ph -> N e. RR )
80 79 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> N e. RR )
81 77 lem1d 
 |-  ( n e. ( 1 ... N ) -> ( n - 1 ) <_ n )
82 81 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n - 1 ) <_ n )
83 elfzle2 
 |-  ( n e. ( 1 ... N ) -> n <_ N )
84 83 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n <_ N )
85 76 78 80 82 84 letrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n - 1 ) <_ N )
86 85 adantrr 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( n - 1 ) <_ N )
87 1 nnzd 
 |-  ( ph -> N e. ZZ )
88 fznn 
 |-  ( N e. ZZ -> ( ( n - 1 ) e. ( 1 ... N ) <-> ( ( n - 1 ) e. NN /\ ( n - 1 ) <_ N ) ) )
89 87 88 syl 
 |-  ( ph -> ( ( n - 1 ) e. ( 1 ... N ) <-> ( ( n - 1 ) e. NN /\ ( n - 1 ) <_ N ) ) )
90 89 adantr 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( ( n - 1 ) e. ( 1 ... N ) <-> ( ( n - 1 ) e. NN /\ ( n - 1 ) <_ N ) ) )
91 74 86 90 mpbir2and 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( n - 1 ) e. ( 1 ... N ) )
92 61 91 sylan 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( n - 1 ) e. ( 1 ... N ) )
93 ovex 
 |-  ( n - 1 ) e. _V
94 eleq1 
 |-  ( m = ( n - 1 ) -> ( m e. ( 1 ... N ) <-> ( n - 1 ) e. ( 1 ... N ) ) )
95 94 anbi2d 
 |-  ( m = ( n - 1 ) -> ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) <-> ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n - 1 ) e. ( 1 ... N ) ) ) )
96 oveq2 
 |-  ( m = ( n - 1 ) -> ( 1 ... m ) = ( 1 ... ( n - 1 ) ) )
97 96 imaeq2d 
 |-  ( m = ( n - 1 ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) )
98 96 imaeq2d 
 |-  ( m = ( n - 1 ) -> ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
99 97 98 eqeq12d 
 |-  ( m = ( n - 1 ) -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) <-> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
100 95 99 imbi12d 
 |-  ( m = ( n - 1 ) -> ( ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) ) <-> ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n - 1 ) e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) ) )
101 93 100 59 vtocl 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n - 1 ) e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
102 92 101 syldan 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
103 102 expr 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( -. n = 1 -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
104 ima0 
 |-  ( ( 2nd ` ( 1st ` z ) ) " (/) ) = (/)
105 ima0 
 |-  ( ( 2nd ` ( 1st ` k ) ) " (/) ) = (/)
106 104 105 eqtr4i 
 |-  ( ( 2nd ` ( 1st ` z ) ) " (/) ) = ( ( 2nd ` ( 1st ` k ) ) " (/) )
107 oveq1 
 |-  ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
108 1m1e0 
 |-  ( 1 - 1 ) = 0
109 107 108 eqtrdi 
 |-  ( n = 1 -> ( n - 1 ) = 0 )
110 109 oveq2d 
 |-  ( n = 1 -> ( 1 ... ( n - 1 ) ) = ( 1 ... 0 ) )
111 fz10 
 |-  ( 1 ... 0 ) = (/)
112 110 111 eqtrdi 
 |-  ( n = 1 -> ( 1 ... ( n - 1 ) ) = (/) )
113 112 imaeq2d 
 |-  ( n = 1 -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` z ) ) " (/) ) )
114 112 imaeq2d 
 |-  ( n = 1 -> ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " (/) ) )
115 106 113 114 3eqtr4a 
 |-  ( n = 1 -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
116 103 115 pm2.61d2 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
117 60 116 difeq12d 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
118 fnsnfv 
 |-  ( ( ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( 2nd ` ( 1st ` z ) ) " { n } ) )
119 24 118 sylan 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( 2nd ` ( 1st ` z ) ) " { n } ) )
120 62 adantl 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> n e. NN )
121 uncom 
 |-  ( ( 1 ... ( n - 1 ) ) u. { n } ) = ( { n } u. ( 1 ... ( n - 1 ) ) )
122 121 difeq1i 
 |-  ( ( ( 1 ... ( n - 1 ) ) u. { n } ) \ ( 1 ... ( n - 1 ) ) ) = ( ( { n } u. ( 1 ... ( n - 1 ) ) ) \ ( 1 ... ( n - 1 ) ) )
123 difun2 
 |-  ( ( { n } u. ( 1 ... ( n - 1 ) ) ) \ ( 1 ... ( n - 1 ) ) ) = ( { n } \ ( 1 ... ( n - 1 ) ) )
124 122 123 eqtri 
 |-  ( ( ( 1 ... ( n - 1 ) ) u. { n } ) \ ( 1 ... ( n - 1 ) ) ) = ( { n } \ ( 1 ... ( n - 1 ) ) )
125 nncn 
 |-  ( n e. NN -> n e. CC )
126 npcan1 
 |-  ( n e. CC -> ( ( n - 1 ) + 1 ) = n )
127 125 126 syl 
 |-  ( n e. NN -> ( ( n - 1 ) + 1 ) = n )
128 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
129 128 biimpi 
 |-  ( n e. NN -> n e. ( ZZ>= ` 1 ) )
130 127 129 eqeltrd 
 |-  ( n e. NN -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
131 63 nn0zd 
 |-  ( n e. NN -> ( n - 1 ) e. ZZ )
132 uzid 
 |-  ( ( n - 1 ) e. ZZ -> ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
133 131 132 syl 
 |-  ( n e. NN -> ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
134 peano2uz 
 |-  ( ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
135 133 134 syl 
 |-  ( n e. NN -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
136 127 135 eqeltrrd 
 |-  ( n e. NN -> n e. ( ZZ>= ` ( n - 1 ) ) )
137 fzsplit2 
 |-  ( ( ( ( n - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` ( n - 1 ) ) ) -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) )
138 130 136 137 syl2anc 
 |-  ( n e. NN -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) )
139 127 oveq1d 
 |-  ( n e. NN -> ( ( ( n - 1 ) + 1 ) ... n ) = ( n ... n ) )
140 nnz 
 |-  ( n e. NN -> n e. ZZ )
141 fzsn 
 |-  ( n e. ZZ -> ( n ... n ) = { n } )
142 140 141 syl 
 |-  ( n e. NN -> ( n ... n ) = { n } )
143 139 142 eqtrd 
 |-  ( n e. NN -> ( ( ( n - 1 ) + 1 ) ... n ) = { n } )
144 143 uneq2d 
 |-  ( n e. NN -> ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) = ( ( 1 ... ( n - 1 ) ) u. { n } ) )
145 138 144 eqtrd 
 |-  ( n e. NN -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. { n } ) )
146 145 difeq1d 
 |-  ( n e. NN -> ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) = ( ( ( 1 ... ( n - 1 ) ) u. { n } ) \ ( 1 ... ( n - 1 ) ) ) )
147 nnre 
 |-  ( n e. NN -> n e. RR )
148 ltm1 
 |-  ( n e. RR -> ( n - 1 ) < n )
149 peano2rem 
 |-  ( n e. RR -> ( n - 1 ) e. RR )
150 ltnle 
 |-  ( ( ( n - 1 ) e. RR /\ n e. RR ) -> ( ( n - 1 ) < n <-> -. n <_ ( n - 1 ) ) )
151 149 150 mpancom 
 |-  ( n e. RR -> ( ( n - 1 ) < n <-> -. n <_ ( n - 1 ) ) )
152 148 151 mpbid 
 |-  ( n e. RR -> -. n <_ ( n - 1 ) )
153 elfzle2 
 |-  ( n e. ( 1 ... ( n - 1 ) ) -> n <_ ( n - 1 ) )
154 152 153 nsyl 
 |-  ( n e. RR -> -. n e. ( 1 ... ( n - 1 ) ) )
155 147 154 syl 
 |-  ( n e. NN -> -. n e. ( 1 ... ( n - 1 ) ) )
156 incom 
 |-  ( ( 1 ... ( n - 1 ) ) i^i { n } ) = ( { n } i^i ( 1 ... ( n - 1 ) ) )
157 156 eqeq1i 
 |-  ( ( ( 1 ... ( n - 1 ) ) i^i { n } ) = (/) <-> ( { n } i^i ( 1 ... ( n - 1 ) ) ) = (/) )
158 disjsn 
 |-  ( ( ( 1 ... ( n - 1 ) ) i^i { n } ) = (/) <-> -. n e. ( 1 ... ( n - 1 ) ) )
159 disj3 
 |-  ( ( { n } i^i ( 1 ... ( n - 1 ) ) ) = (/) <-> { n } = ( { n } \ ( 1 ... ( n - 1 ) ) ) )
160 157 158 159 3bitr3i 
 |-  ( -. n e. ( 1 ... ( n - 1 ) ) <-> { n } = ( { n } \ ( 1 ... ( n - 1 ) ) ) )
161 155 160 sylib 
 |-  ( n e. NN -> { n } = ( { n } \ ( 1 ... ( n - 1 ) ) ) )
162 124 146 161 3eqtr4a 
 |-  ( n e. NN -> ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) = { n } )
163 120 162 syl 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) = { n } )
164 163 imaeq2d 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) ) = ( ( 2nd ` ( 1st ` z ) ) " { n } ) )
165 dff1o3 
 |-  ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` z ) ) ) )
166 165 simprbi 
 |-  ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` z ) ) )
167 22 166 syl 
 |-  ( z e. S -> Fun `' ( 2nd ` ( 1st ` z ) ) )
168 imadif 
 |-  ( Fun `' ( 2nd ` ( 1st ` z ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
169 167 168 syl 
 |-  ( z e. S -> ( ( 2nd ` ( 1st ` z ) ) " ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
170 169 adantr 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
171 119 164 170 3eqtr2d 
 |-  ( ( z e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
172 6 171 sylan 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
173 eleq1 
 |-  ( z = k -> ( z e. S <-> k e. S ) )
174 173 anbi1d 
 |-  ( z = k -> ( ( z e. S /\ n e. ( 1 ... N ) ) <-> ( k e. S /\ n e. ( 1 ... N ) ) ) )
175 2fveq3 
 |-  ( z = k -> ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) )
176 175 fveq1d 
 |-  ( z = k -> ( ( 2nd ` ( 1st ` z ) ) ` n ) = ( ( 2nd ` ( 1st ` k ) ) ` n ) )
177 176 sneqd 
 |-  ( z = k -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = { ( ( 2nd ` ( 1st ` k ) ) ` n ) } )
178 175 imaeq1d 
 |-  ( z = k -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) )
179 175 imaeq1d 
 |-  ( z = k -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
180 178 179 difeq12d 
 |-  ( z = k -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
181 177 180 eqeq12d 
 |-  ( z = k -> ( { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) <-> { ( ( 2nd ` ( 1st ` k ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) ) )
182 174 181 imbi12d 
 |-  ( z = k -> ( ( ( z e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) ) <-> ( ( k e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` k ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) ) ) )
183 182 171 chvarvv 
 |-  ( ( k e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` k ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
184 9 183 sylan 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` k ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
185 117 172 184 3eqtr4d 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = { ( ( 2nd ` ( 1st ` k ) ) ` n ) } )
186 fvex 
 |-  ( ( 2nd ` ( 1st ` z ) ) ` n ) e. _V
187 186 sneqr 
 |-  ( { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = { ( ( 2nd ` ( 1st ` k ) ) ` n ) } -> ( ( 2nd ` ( 1st ` z ) ) ` n ) = ( ( 2nd ` ( 1st ` k ) ) ` n ) )
188 185 187 syl 
 |-  ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) ` n ) = ( ( 2nd ` ( 1st ` k ) ) ` n ) )
189 26 40 188 eqfnfvd 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) )
190 xpopth 
 |-  ( ( ( 1st ` z ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( 1st ` k ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` k ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) ) <-> ( 1st ` z ) = ( 1st ` k ) ) )
191 16 30 190 syl2an 
 |-  ( ( z e. S /\ k e. S ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` k ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) ) <-> ( 1st ` z ) = ( 1st ` k ) ) )
192 191 ad2antlr 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` k ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) ) <-> ( 1st ` z ) = ( 1st ` k ) ) )
193 12 189 192 mpbi2and 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 1st ` z ) = ( 1st ` k ) )
194 eqtr3 
 |-  ( ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) -> ( 2nd ` z ) = ( 2nd ` k ) )
195 194 adantl 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` z ) = ( 2nd ` k ) )
196 xpopth 
 |-  ( ( z e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ k e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( ( 1st ` z ) = ( 1st ` k ) /\ ( 2nd ` z ) = ( 2nd ` k ) ) <-> z = k ) )
197 14 28 196 syl2an 
 |-  ( ( z e. S /\ k e. S ) -> ( ( ( 1st ` z ) = ( 1st ` k ) /\ ( 2nd ` z ) = ( 2nd ` k ) ) <-> z = k ) )
198 197 ad2antlr 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( ( ( 1st ` z ) = ( 1st ` k ) /\ ( 2nd ` z ) = ( 2nd ` k ) ) <-> z = k ) )
199 193 195 198 mpbi2and 
 |-  ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> z = k )
200 199 ex 
 |-  ( ( ph /\ ( z e. S /\ k e. S ) ) -> ( ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) -> z = k ) )
201 200 ralrimivva 
 |-  ( ph -> A. z e. S A. k e. S ( ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) -> z = k ) )
202 fveqeq2 
 |-  ( z = k -> ( ( 2nd ` z ) = 0 <-> ( 2nd ` k ) = 0 ) )
203 202 rmo4 
 |-  ( E* z e. S ( 2nd ` z ) = 0 <-> A. z e. S A. k e. S ( ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) -> z = k ) )
204 201 203 sylibr 
 |-  ( ph -> E* z e. S ( 2nd ` z ) = 0 )