Metamath Proof Explorer

Theorem poimirlem14

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

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