Metamath Proof Explorer

Theorem poimirlem26

Description: Lemma for poimir showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) of Kulpa p. 548. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem28.1 
|- ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
poimirlem28.2 
|- ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
Assertion poimirlem26 
|- ( ph -> 2 || ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem28.1 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
3 poimirlem28.2 
 |-  ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
4 fzofi 
 |-  ( 0 ..^ K ) e. Fin
5 fzfi 
 |-  ( 1 ... N ) e. Fin
6 mapfi 
 |-  ( ( ( 0 ..^ K ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 0 ..^ K ) ^m ( 1 ... N ) ) e. Fin )
7 4 5 6 mp2an 
 |-  ( ( 0 ..^ K ) ^m ( 1 ... N ) ) e. Fin
8 mapfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin )
9 5 5 8 mp2an 
 |-  ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin
10 f1of 
 |-  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> f : ( 1 ... N ) --> ( 1 ... N ) )
11 10 ss2abi 
 |-  { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ { f | f : ( 1 ... N ) --> ( 1 ... N ) }
12 ovex 
 |-  ( 1 ... N ) e. _V
13 12 12 mapval 
 |-  ( ( 1 ... N ) ^m ( 1 ... N ) ) = { f | f : ( 1 ... N ) --> ( 1 ... N ) }
14 11 13 sseqtrri 
 |-  { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ ( ( 1 ... N ) ^m ( 1 ... N ) )
15 ssfi 
 |-  ( ( ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin /\ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ ( ( 1 ... N ) ^m ( 1 ... N ) ) ) -> { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin )
16 9 14 15 mp2an 
 |-  { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin
17 7 16 pm3.2i 
 |-  ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) e. Fin /\ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin )
18 xpfi 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) e. Fin /\ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin ) -> ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. Fin )
19 17 18 mp1i 
 |-  ( ph -> ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. Fin )
20 2z 
 |-  2 e. ZZ
21 20 a1i 
 |-  ( ph -> 2 e. ZZ )
22 snfi 
 |-  { x } e. Fin
23 fzfi 
 |-  ( 0 ... N ) e. Fin
24 rabfi 
 |-  ( ( 0 ... N ) e. Fin -> { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } e. Fin )
25 23 24 ax-mp 
 |-  { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } e. Fin
26 xpfi 
 |-  ( ( { x } e. Fin /\ { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } e. Fin ) -> ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) e. Fin )
27 22 25 26 mp2an 
 |-  ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) e. Fin
28 hashcl 
 |-  ( ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) e. Fin -> ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) e. NN0 )
29 27 28 ax-mp 
 |-  ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) e. NN0
30 29 nn0zi 
 |-  ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) e. ZZ
31 30 a1i 
 |-  ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) e. ZZ )
32 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> N e. NN )
33 nfv 
 |-  F/ j p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) )
34 nfcsb1v 
 |-  F/_ j [_ k / j ]_ [_ t / s ]_ C
35 34 nfeq2 
 |-  F/ j B = [_ k / j ]_ [_ t / s ]_ C
36 33 35 nfim 
 |-  F/ j ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ k / j ]_ [_ t / s ]_ C )
37 oveq2 
 |-  ( j = k -> ( 1 ... j ) = ( 1 ... k ) )
38 37 imaeq2d 
 |-  ( j = k -> ( ( 2nd ` t ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... k ) ) )
39 38 xpeq1d 
 |-  ( j = k -> ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) )
40 oveq1 
 |-  ( j = k -> ( j + 1 ) = ( k + 1 ) )
41 40 oveq1d 
 |-  ( j = k -> ( ( j + 1 ) ... N ) = ( ( k + 1 ) ... N ) )
42 41 imaeq2d 
 |-  ( j = k -> ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) )
43 42 xpeq1d 
 |-  ( j = k -> ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) )
44 39 43 uneq12d 
 |-  ( j = k -> ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) )
45 44 oveq2d 
 |-  ( j = k -> ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) ) )
46 45 eqeq2d 
 |-  ( j = k -> ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) <-> p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
47 csbeq1a 
 |-  ( j = k -> [_ t / s ]_ C = [_ k / j ]_ [_ t / s ]_ C )
48 47 eqeq2d 
 |-  ( j = k -> ( B = [_ t / s ]_ C <-> B = [_ k / j ]_ [_ t / s ]_ C ) )
49 46 48 imbi12d 
 |-  ( j = k -> ( ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ t / s ]_ C ) <-> ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ k / j ]_ [_ t / s ]_ C ) ) )
50 nfv 
 |-  F/ s p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
51 nfcsb1v 
 |-  F/_ s [_ t / s ]_ C
52 51 nfeq2 
 |-  F/ s B = [_ t / s ]_ C
53 50 52 nfim 
 |-  F/ s ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ t / s ]_ C )
54 fveq2 
 |-  ( s = t -> ( 1st ` s ) = ( 1st ` t ) )
55 fveq2 
 |-  ( s = t -> ( 2nd ` s ) = ( 2nd ` t ) )
56 55 imaeq1d 
 |-  ( s = t -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... j ) ) )
57 56 xpeq1d 
 |-  ( s = t -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) )
58 55 imaeq1d 
 |-  ( s = t -> ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) )
59 58 xpeq1d 
 |-  ( s = t -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
60 57 59 uneq12d 
 |-  ( s = t -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
61 54 60 oveq12d 
 |-  ( s = t -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
62 61 eqeq2d 
 |-  ( s = t -> ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) <-> p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
63 csbeq1a 
 |-  ( s = t -> C = [_ t / s ]_ C )
64 63 eqeq2d 
 |-  ( s = t -> ( B = C <-> B = [_ t / s ]_ C ) )
65 62 64 imbi12d 
 |-  ( s = t -> ( ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C ) <-> ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ t / s ]_ C ) ) )
66 53 65 2 chvarfv 
 |-  ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ t / s ]_ C )
67 36 49 66 chvarfv 
 |-  ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ k / j ]_ [_ t / s ]_ C )
68 3 ad4ant14 
 |-  ( ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
69 xp1st 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` x ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
70 elmapi 
 |-  ( ( 1st ` x ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` x ) : ( 1 ... N ) --> ( 0 ..^ K ) )
71 69 70 syl 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` x ) : ( 1 ... N ) --> ( 0 ..^ K ) )
72 71 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> ( 1st ` x ) : ( 1 ... N ) --> ( 0 ..^ K ) )
73 xp2nd 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` x ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
74 fvex 
 |-  ( 2nd ` x ) e. _V
75 f1oeq1 
 |-  ( f = ( 2nd ` x ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` x ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
76 74 75 elab 
 |-  ( ( 2nd ` x ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` x ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
77 73 76 sylib 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` x ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
78 77 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> ( 2nd ` x ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
79 nfcv 
 |-  F/_ j N
80 nfcv 
 |-  F/_ j x
81 80 34 nfcsbw 
 |-  F/_ j [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
82 79 81 nfne 
 |-  F/ j N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
83 nfcv 
 |-  F/_ t C
84 83 51 63 cbvcsbw 
 |-  [_ x / s ]_ C = [_ x / t ]_ [_ t / s ]_ C
85 47 csbeq2dv 
 |-  ( j = k -> [_ x / t ]_ [_ t / s ]_ C = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
86 84 85 syl5eq 
 |-  ( j = k -> [_ x / s ]_ C = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
87 86 neeq2d 
 |-  ( j = k -> ( N =/= [_ x / s ]_ C <-> N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
88 82 87 rspc 
 |-  ( k e. ( 0 ... N ) -> ( A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
89 88 impcom 
 |-  ( ( A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C /\ k e. ( 0 ... N ) ) -> N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
90 89 adantll 
 |-  ( ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) /\ k e. ( 0 ... N ) ) -> N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
91 1st2nd2 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
92 91 csbeq1d 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C )
93 92 ad3antlr 
 |-  ( ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) /\ k e. ( 0 ... N ) ) -> [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C )
94 90 93 neeqtrd 
 |-  ( ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) /\ k e. ( 0 ... N ) ) -> N =/= [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C )
95 32 67 68 72 78 94 poimirlem25 
 |-  ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> 2 || ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. k e. ( ( 0 ... N ) \ { y } ) i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C } ) )
96 nfv 
 |-  F/ k i = [_ x / s ]_ C
97 81 nfeq2 
 |-  F/ j i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
98 86 eqeq2d 
 |-  ( j = k -> ( i = [_ x / s ]_ C <-> i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
99 96 97 98 cbvrexw 
 |-  ( E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C <-> E. k e. ( ( 0 ... N ) \ { y } ) i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
100 92 eqeq2d 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C <-> i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
101 100 rexbidv 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( E. k e. ( ( 0 ... N ) \ { y } ) i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C <-> E. k e. ( ( 0 ... N ) \ { y } ) i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
102 99 101 bitr2id 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( E. k e. ( ( 0 ... N ) \ { y } ) i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C ) )
103 102 ralbidv 
 |-  ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. k e. ( ( 0 ... N ) \ { y } ) i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C ) )
104 iba 
 |-  ( A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) )
105 103 104 sylan9bb 
 |-  ( ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. k e. ( ( 0 ... N ) \ { y } ) i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) )
106 105 rabbidv 
 |-  ( ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. k e. ( ( 0 ... N ) \ { y } ) i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C } = { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } )
107 106 fveq2d 
 |-  ( ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. k e. ( ( 0 ... N ) \ { y } ) i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C } ) = ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
108 107 adantll 
 |-  ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. k e. ( ( 0 ... N ) \ { y } ) i = [_ <. ( 1st ` x ) , ( 2nd ` x ) >. / t ]_ [_ k / j ]_ [_ t / s ]_ C } ) = ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
109 95 108 breqtrd 
 |-  ( ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> 2 || ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
110 109 ex 
 |-  ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> ( A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> 2 || ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) )
111 dvds0 
 |-  ( 2 e. ZZ -> 2 || 0 )
112 20 111 ax-mp 
 |-  2 || 0
113 hash0 
 |-  ( # ` (/) ) = 0
114 112 113 breqtrri 
 |-  2 || ( # ` (/) )
115 simpr 
 |-  ( ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) -> A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C )
116 115 con3i 
 |-  ( -. A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> -. ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) )
117 116 ralrimivw 
 |-  ( -. A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> A. y e. ( 0 ... N ) -. ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) )
118 rabeq0 
 |-  ( { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } = (/) <-> A. y e. ( 0 ... N ) -. ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) )
119 117 118 sylibr 
 |-  ( -. A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } = (/) )
120 119 fveq2d 
 |-  ( -. A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) = ( # ` (/) ) )
121 114 120 breqtrrid 
 |-  ( -. A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> 2 || ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
122 110 121 pm2.61d1 
 |-  ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> 2 || ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
123 hashxp 
 |-  ( ( { x } e. Fin /\ { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } e. Fin ) -> ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) = ( ( # ` { x } ) x. ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) )
124 22 25 123 mp2an 
 |-  ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) = ( ( # ` { x } ) x. ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
125 vex 
 |-  x e. _V
126 hashsng 
 |-  ( x e. _V -> ( # ` { x } ) = 1 )
127 125 126 ax-mp 
 |-  ( # ` { x } ) = 1
128 127 oveq1i 
 |-  ( ( # ` { x } ) x. ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) = ( 1 x. ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
129 hashcl 
 |-  ( { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } e. Fin -> ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) e. NN0 )
130 25 129 ax-mp 
 |-  ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) e. NN0
131 130 nn0cni 
 |-  ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) e. CC
132 131 mulid2i 
 |-  ( 1 x. ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) = ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } )
133 124 128 132 3eqtri 
 |-  ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) = ( # ` { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } )
134 122 133 breqtrrdi 
 |-  ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> 2 || ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) )
135 19 21 31 134 fsumdvds 
 |-  ( ph -> 2 || sum_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) )
136 7 16 18 mp2an 
 |-  ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. Fin
137 xpfi 
 |-  ( ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. Fin /\ ( 0 ... N ) e. Fin ) -> ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) e. Fin )
138 136 23 137 mp2an 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) e. Fin
139 rabfi 
 |-  ( ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) e. Fin -> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } e. Fin )
140 138 139 ax-mp 
 |-  { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } e. Fin
141 1 nncnd 
 |-  ( ph -> N e. CC )
142 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
143 141 142 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
144 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
145 1 144 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
146 145 nn0zd 
 |-  ( ph -> ( N - 1 ) e. ZZ )
147 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
148 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
149 146 147 148 3syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
150 143 149 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
151 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
152 ssralv 
 |-  ( ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
153 150 151 152 3syl 
 |-  ( ph -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
154 153 adantr 
 |-  ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
155 raldifb 
 |-  ( A. j e. ( 0 ... N ) ( j e/ { ( 2nd ` t ) } -> -. i = [_ ( 1st ` t ) / s ]_ C ) <-> A. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) -. i = [_ ( 1st ` t ) / s ]_ C )
156 nfv 
 |-  F/ j ph
157 nfcsb1v 
 |-  F/_ j [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C
158 157 nfeq2 
 |-  F/ j N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C
159 156 158 nfan 
 |-  F/ j ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
160 nfv 
 |-  F/ j i e. ( 0 ... ( N - 1 ) )
161 159 160 nfan 
 |-  F/ j ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) )
162 nnel 
 |-  ( -. j e/ { ( 2nd ` t ) } <-> j e. { ( 2nd ` t ) } )
163 velsn 
 |-  ( j e. { ( 2nd ` t ) } <-> j = ( 2nd ` t ) )
164 162 163 bitri 
 |-  ( -. j e/ { ( 2nd ` t ) } <-> j = ( 2nd ` t ) )
165 csbeq1a 
 |-  ( j = ( 2nd ` t ) -> [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
166 165 eqeq2d 
 |-  ( j = ( 2nd ` t ) -> ( N = [_ ( 1st ` t ) / s ]_ C <-> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
167 166 biimparc 
 |-  ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ j = ( 2nd ` t ) ) -> N = [_ ( 1st ` t ) / s ]_ C )
168 1 nnred 
 |-  ( ph -> N e. RR )
169 168 ltm1d 
 |-  ( ph -> ( N - 1 ) < N )
170 145 nn0red 
 |-  ( ph -> ( N - 1 ) e. RR )
171 170 168 ltnled 
 |-  ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
172 169 171 mpbid 
 |-  ( ph -> -. N <_ ( N - 1 ) )
173 elfzle2 
 |-  ( N e. ( 0 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
174 172 173 nsyl 
 |-  ( ph -> -. N e. ( 0 ... ( N - 1 ) ) )
175 eleq1 
 |-  ( i = N -> ( i e. ( 0 ... ( N - 1 ) ) <-> N e. ( 0 ... ( N - 1 ) ) ) )
176 175 notbid 
 |-  ( i = N -> ( -. i e. ( 0 ... ( N - 1 ) ) <-> -. N e. ( 0 ... ( N - 1 ) ) ) )
177 174 176 syl5ibrcom 
 |-  ( ph -> ( i = N -> -. i e. ( 0 ... ( N - 1 ) ) ) )
178 177 con2d 
 |-  ( ph -> ( i e. ( 0 ... ( N - 1 ) ) -> -. i = N ) )
179 178 imp 
 |-  ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) -> -. i = N )
180 eqeq2 
 |-  ( N = [_ ( 1st ` t ) / s ]_ C -> ( i = N <-> i = [_ ( 1st ` t ) / s ]_ C ) )
181 180 notbid 
 |-  ( N = [_ ( 1st ` t ) / s ]_ C -> ( -. i = N <-> -. i = [_ ( 1st ` t ) / s ]_ C ) )
182 179 181 syl5ibcom 
 |-  ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( N = [_ ( 1st ` t ) / s ]_ C -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
183 167 182 syl5 
 |-  ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ j = ( 2nd ` t ) ) -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
184 183 expdimp 
 |-  ( ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) -> ( j = ( 2nd ` t ) -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
185 184 an32s 
 |-  ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( j = ( 2nd ` t ) -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
186 164 185 syl5bi 
 |-  ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( -. j e/ { ( 2nd ` t ) } -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
187 idd 
 |-  ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( -. i = [_ ( 1st ` t ) / s ]_ C -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
188 186 187 jad 
 |-  ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( ( j e/ { ( 2nd ` t ) } -> -. i = [_ ( 1st ` t ) / s ]_ C ) -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
189 188 adantr 
 |-  ( ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( j e/ { ( 2nd ` t ) } -> -. i = [_ ( 1st ` t ) / s ]_ C ) -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
190 161 189 ralimdaa 
 |-  ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( A. j e. ( 0 ... N ) ( j e/ { ( 2nd ` t ) } -> -. i = [_ ( 1st ` t ) / s ]_ C ) -> A. j e. ( 0 ... N ) -. i = [_ ( 1st ` t ) / s ]_ C ) )
191 155 190 syl5bir 
 |-  ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( A. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) -. i = [_ ( 1st ` t ) / s ]_ C -> A. j e. ( 0 ... N ) -. i = [_ ( 1st ` t ) / s ]_ C ) )
192 191 con3d 
 |-  ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( -. A. j e. ( 0 ... N ) -. i = [_ ( 1st ` t ) / s ]_ C -> -. A. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) -. i = [_ ( 1st ` t ) / s ]_ C ) )
193 dfrex2 
 |-  ( E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> -. A. j e. ( 0 ... N ) -. i = [_ ( 1st ` t ) / s ]_ C )
194 dfrex2 
 |-  ( E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C <-> -. A. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) -. i = [_ ( 1st ` t ) / s ]_ C )
195 192 193 194 3imtr4g 
 |-  ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C -> E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) )
196 195 ralimdva 
 |-  ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) )
197 154 196 syld 
 |-  ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) )
198 197 expimpd 
 |-  ( ph -> ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) )
199 198 adantr 
 |-  ( ( ph /\ t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) )
200 199 ss2rabdv 
 |-  ( ph -> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } C_ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } )
201 hashssdif 
 |-  ( ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } e. Fin /\ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } C_ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } ) -> ( # ` ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } \ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) = ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } ) - ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) )
202 140 200 201 sylancr 
 |-  ( ph -> ( # ` ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } \ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) = ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } ) - ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) )
203 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 ) )
204 df-ne 
 |-  ( N =/= [_ ( 1st ` t ) / s ]_ C <-> -. N = [_ ( 1st ` t ) / s ]_ C )
205 204 ralbii 
 |-  ( A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C <-> A. j e. ( 0 ... N ) -. N = [_ ( 1st ` t ) / s ]_ C )
206 ralnex 
 |-  ( A. j e. ( 0 ... N ) -. N = [_ ( 1st ` t ) / s ]_ C <-> -. E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C )
207 205 206 bitri 
 |-  ( A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C <-> -. E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C )
208 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
209 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
210 208 209 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
211 143 210 eqeltrd 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 0 ) )
212 fzsplit2 
 |-  ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 0 ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
213 211 150 212 syl2anc 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
214 143 oveq1d 
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
215 1 nnzd 
 |-  ( ph -> N e. ZZ )
216 fzsn 
 |-  ( N e. ZZ -> ( N ... N ) = { N } )
217 215 216 syl 
 |-  ( ph -> ( N ... N ) = { N } )
218 214 217 eqtrd 
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
219 218 uneq2d 
 |-  ( ph -> ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( 0 ... ( N - 1 ) ) u. { N } ) )
220 213 219 eqtrd 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. { N } ) )
221 220 raleqdv 
 |-  ( ph -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> A. i e. ( ( 0 ... ( N - 1 ) ) u. { N } ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
222 ralunb 
 |-  ( A. i e. ( ( 0 ... ( N - 1 ) ) u. { N } ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C /\ A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
223 difss 
 |-  ( ( 0 ... N ) \ { ( 2nd ` t ) } ) C_ ( 0 ... N )
224 ssrexv 
 |-  ( ( ( 0 ... N ) \ { ( 2nd ` t ) } ) C_ ( 0 ... N ) -> ( E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
225 223 224 ax-mp 
 |-  ( E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C )
226 225 ralimi 
 |-  ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C )
227 226 biantrurd 
 |-  ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> ( A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C /\ A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) )
228 222 227 bitr4id 
 |-  ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> ( A. i e. ( ( 0 ... ( N - 1 ) ) u. { N } ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
229 221 228 sylan9bb 
 |-  ( ( ph /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
230 229 adantlr 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) )
231 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
232 208 231 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
233 232 ad2antrr 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> N e. ( 0 ... N ) )
234 eqeq1 
 |-  ( i = N -> ( i = [_ ( 1st ` t ) / s ]_ C <-> N = [_ ( 1st ` t ) / s ]_ C ) )
235 234 rexbidv 
 |-  ( i = N -> ( E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C ) )
236 235 rspcva 
 |-  ( ( N e. ( 0 ... N ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) -> E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C )
237 nfv 
 |-  F/ j ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) )
238 nfcv 
 |-  F/_ j ( 0 ... ( N - 1 ) )
239 nfre1 
 |-  F/ j E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C
240 238 239 nfralw 
 |-  F/ j A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C
241 237 240 nfan 
 |-  F/ j ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C )
242 eleq1 
 |-  ( N = [_ ( 1st ` t ) / s ]_ C -> ( N e. ( 0 ... ( N - 1 ) ) <-> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
243 242 notbid 
 |-  ( N = [_ ( 1st ` t ) / s ]_ C -> ( -. N e. ( 0 ... ( N - 1 ) ) <-> -. [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
244 174 243 syl5ibcom 
 |-  ( ph -> ( N = [_ ( 1st ` t ) / s ]_ C -> -. [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
245 244 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( 0 ... N ) ) -> ( N = [_ ( 1st ` t ) / s ]_ C -> -. [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
246 eldifsn 
 |-  ( j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) <-> ( j e. ( 0 ... N ) /\ j =/= ( 2nd ` t ) ) )
247 diffi 
 |-  ( ( 0 ... N ) e. Fin -> ( ( 0 ... N ) \ { ( 2nd ` t ) } ) e. Fin )
248 23 247 ax-mp 
 |-  ( ( 0 ... N ) \ { ( 2nd ` t ) } ) e. Fin
249 ssrab2 
 |-  { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } C_ ( ( 0 ... N ) \ { ( 2nd ` t ) } )
250 ssdomg 
 |-  ( ( ( 0 ... N ) \ { ( 2nd ` t ) } ) e. Fin -> ( { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } C_ ( ( 0 ... N ) \ { ( 2nd ` t ) } ) -> { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ~<_ ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) )
251 248 249 250 mp2 
 |-  { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ~<_ ( ( 0 ... N ) \ { ( 2nd ` t ) } )
252 hashdifsn 
 |-  ( ( ( 0 ... N ) e. Fin /\ ( 2nd ` t ) e. ( 0 ... N ) ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( ( # ` ( 0 ... N ) ) - 1 ) )
253 23 252 mpan 
 |-  ( ( 2nd ` t ) e. ( 0 ... N ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( ( # ` ( 0 ... N ) ) - 1 ) )
254 1cnd 
 |-  ( ph -> 1 e. CC )
255 141 254 254 addsubd 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = ( ( N - 1 ) + 1 ) )
256 hashfz0 
 |-  ( N e. NN0 -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
257 208 256 syl 
 |-  ( ph -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
258 257 oveq1d 
 |-  ( ph -> ( ( # ` ( 0 ... N ) ) - 1 ) = ( ( N + 1 ) - 1 ) )
259 hashfz0 
 |-  ( ( N - 1 ) e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( ( N - 1 ) + 1 ) )
260 145 259 syl 
 |-  ( ph -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( ( N - 1 ) + 1 ) )
261 255 258 260 3eqtr4d 
 |-  ( ph -> ( ( # ` ( 0 ... N ) ) - 1 ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
262 253 261 sylan9eqr 
 |-  ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
263 fzfi 
 |-  ( 0 ... ( N - 1 ) ) e. Fin
264 hashen 
 |-  ( ( ( ( 0 ... N ) \ { ( 2nd ` t ) } ) e. Fin /\ ( 0 ... ( N - 1 ) ) e. Fin ) -> ( ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( # ` ( 0 ... ( N - 1 ) ) ) <-> ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ~~ ( 0 ... ( N - 1 ) ) ) )
265 248 263 264 mp2an 
 |-  ( ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( # ` ( 0 ... ( N - 1 ) ) ) <-> ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ~~ ( 0 ... ( N - 1 ) ) )
266 262 265 sylib 
 |-  ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) -> ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ~~ ( 0 ... ( N - 1 ) ) )
267 rabfi 
 |-  ( ( ( 0 ... N ) \ { ( 2nd ` t ) } ) e. Fin -> { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } e. Fin )
268 248 267 ax-mp 
 |-  { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } e. Fin
269 eleq1 
 |-  ( i = [_ ( 1st ` t ) / s ]_ C -> ( i e. ( 0 ... ( N - 1 ) ) <-> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
270 269 biimpac 
 |-  ( ( i e. ( 0 ... ( N - 1 ) ) /\ i = [_ ( 1st ` t ) / s ]_ C ) -> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) )
271 rabid 
 |-  ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } <-> ( j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) /\ [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
272 271 simplbi2com 
 |-  ( [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) -> ( j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) -> j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ) )
273 270 272 syl 
 |-  ( ( i e. ( 0 ... ( N - 1 ) ) /\ i = [_ ( 1st ` t ) / s ]_ C ) -> ( j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) -> j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ) )
274 273 impancom 
 |-  ( ( i e. ( 0 ... ( N - 1 ) ) /\ j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) -> ( i = [_ ( 1st ` t ) / s ]_ C -> j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ) )
275 274 ancrd 
 |-  ( ( i e. ( 0 ... ( N - 1 ) ) /\ j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) -> ( i = [_ ( 1st ` t ) / s ]_ C -> ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) ) )
276 275 expimpd 
 |-  ( i e. ( 0 ... ( N - 1 ) ) -> ( ( j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) /\ i = [_ ( 1st ` t ) / s ]_ C ) -> ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) ) )
277 276 reximdv2 
 |-  ( i e. ( 0 ... ( N - 1 ) ) -> ( E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> E. j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } i = [_ ( 1st ` t ) / s ]_ C ) )
278 271 simplbi 
 |-  ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } -> j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) )
279 274 pm4.71rd 
 |-  ( ( i e. ( 0 ... ( N - 1 ) ) /\ j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) -> ( i = [_ ( 1st ` t ) / s ]_ C <-> ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) ) )
280 df-mpt 
 |-  ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) = { <. k , i >. | ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) }
281 nfv 
 |-  F/ k ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C )
282 nfrab1 
 |-  F/_ j { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) }
283 282 nfcri 
 |-  F/ j k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) }
284 nfcsb1v 
 |-  F/_ j [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C
285 284 nfeq2 
 |-  F/ j i = [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C
286 283 285 nfan 
 |-  F/ j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C )
287 eleq1 
 |-  ( j = k -> ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } <-> k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ) )
288 csbeq1a 
 |-  ( j = k -> [_ ( 1st ` t ) / s ]_ C = [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C )
289 288 eqeq2d 
 |-  ( j = k -> ( i = [_ ( 1st ` t ) / s ]_ C <-> i = [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
290 287 289 anbi12d 
 |-  ( j = k -> ( ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) <-> ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) ) )
291 281 286 290 cbvopab1 
 |-  { <. j , i >. | ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) } = { <. k , i >. | ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) }
292 280 291 eqtr4i 
 |-  ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) = { <. j , i >. | ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) }
293 292 breqi 
 |-  ( j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i <-> j { <. j , i >. | ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) } i )
294 df-br 
 |-  ( j { <. j , i >. | ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) } i <-> <. j , i >. e. { <. j , i >. | ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) } )
295 opabidw 
 |-  ( <. j , i >. e. { <. j , i >. | ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) } <-> ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) )
296 293 294 295 3bitri 
 |-  ( j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i <-> ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } /\ i = [_ ( 1st ` t ) / s ]_ C ) )
297 279 296 bitr4di 
 |-  ( ( i e. ( 0 ... ( N - 1 ) ) /\ j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) -> ( i = [_ ( 1st ` t ) / s ]_ C <-> j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i ) )
298 278 297 sylan2 
 |-  ( ( i e. ( 0 ... ( N - 1 ) ) /\ j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ) -> ( i = [_ ( 1st ` t ) / s ]_ C <-> j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i ) )
299 298 rexbidva 
 |-  ( i e. ( 0 ... ( N - 1 ) ) -> ( E. j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } i = [_ ( 1st ` t ) / s ]_ C <-> E. j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i ) )
300 nfcv 
 |-  F/_ p { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) }
301 nfv 
 |-  F/ p j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i
302 nfcv 
 |-  F/_ j p
303 282 284 nfmpt 
 |-  F/_ j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C )
304 nfcv 
 |-  F/_ j i
305 302 303 304 nfbr 
 |-  F/ j p ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i
306 breq1 
 |-  ( j = p -> ( j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i <-> p ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i ) )
307 282 300 301 305 306 cbvrexfw 
 |-  ( E. j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } j ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i <-> E. p e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } p ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i )
308 299 307 bitrdi 
 |-  ( i e. ( 0 ... ( N - 1 ) ) -> ( E. j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } i = [_ ( 1st ` t ) / s ]_ C <-> E. p e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } p ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i ) )
309 277 308 sylibd 
 |-  ( i e. ( 0 ... ( N - 1 ) ) -> ( E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> E. p e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } p ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i ) )
310 309 ralimia 
 |-  ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> A. i e. ( 0 ... ( N - 1 ) ) E. p e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } p ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i )
311 eqid 
 |-  ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) = ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C )
312 nfcv 
 |-  F/_ j k
313 nfcv 
 |-  F/_ j ( ( 0 ... N ) \ { ( 2nd ` t ) } )
314 284 nfel1 
 |-  F/ j [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) )
315 288 eleq1d 
 |-  ( j = k -> ( [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) <-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
316 312 313 314 315 elrabf 
 |-  ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } <-> ( k e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) /\ [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
317 316 simprbi 
 |-  ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } -> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) )
318 311 317 fmpti 
 |-  ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) : { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } --> ( 0 ... ( N - 1 ) )
319 310 318 jctil 
 |-  ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> ( ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) : { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } --> ( 0 ... ( N - 1 ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. p e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } p ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i ) )
320 dffo4 
 |-  ( ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) : { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } -onto-> ( 0 ... ( N - 1 ) ) <-> ( ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) : { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } --> ( 0 ... ( N - 1 ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. p e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } p ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) i ) )
321 319 320 sylibr 
 |-  ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) : { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } -onto-> ( 0 ... ( N - 1 ) ) )
322 fodomfi 
 |-  ( ( { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } e. Fin /\ ( k e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } |-> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C ) : { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } -onto-> ( 0 ... ( N - 1 ) ) ) -> ( 0 ... ( N - 1 ) ) ~<_ { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } )
323 268 321 322 sylancr 
 |-  ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> ( 0 ... ( N - 1 ) ) ~<_ { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } )
324 endomtr 
 |-  ( ( ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ~~ ( 0 ... ( N - 1 ) ) /\ ( 0 ... ( N - 1 ) ) ~<_ { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ) -> ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ~<_ { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } )
325 266 323 324 syl2an 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ~<_ { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } )
326 sbth 
 |-  ( ( { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ~<_ ( ( 0 ... N ) \ { ( 2nd ` t ) } ) /\ ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ~<_ { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ) -> { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ~~ ( ( 0 ... N ) \ { ( 2nd ` t ) } ) )
327 251 325 326 sylancr 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ~~ ( ( 0 ... N ) \ { ( 2nd ` t ) } ) )
328 fisseneq 
 |-  ( ( ( ( 0 ... N ) \ { ( 2nd ` t ) } ) e. Fin /\ { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } C_ ( ( 0 ... N ) \ { ( 2nd ` t ) } ) /\ { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ~~ ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) -> { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } = ( ( 0 ... N ) \ { ( 2nd ` t ) } ) )
329 248 249 327 328 mp3an12i 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } = ( ( 0 ... N ) \ { ( 2nd ` t ) } ) )
330 329 eleq2d 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } <-> j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) )
331 330 biimpar 
 |-  ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) -> j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } )
332 288 equcoms 
 |-  ( k = j -> [_ ( 1st ` t ) / s ]_ C = [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C )
333 332 eqcomd 
 |-  ( k = j -> [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C = [_ ( 1st ` t ) / s ]_ C )
334 333 eleq1d 
 |-  ( k = j -> ( [_ k / j ]_ [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) <-> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
335 334 317 vtoclga 
 |-  ( j e. { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } -> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) )
336 331 335 syl 
 |-  ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) -> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) )
337 246 336 sylan2br 
 |-  ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ ( j e. ( 0 ... N ) /\ j =/= ( 2nd ` t ) ) ) -> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) )
338 337 expr 
 |-  ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( 0 ... N ) ) -> ( j =/= ( 2nd ` t ) -> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
339 338 necon1bd 
 |-  ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( 0 ... N ) ) -> ( -. [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) -> j = ( 2nd ` t ) ) )
340 245 339 syld 
 |-  ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( 0 ... N ) ) -> ( N = [_ ( 1st ` t ) / s ]_ C -> j = ( 2nd ` t ) ) )
341 340 imp 
 |-  ( ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( 0 ... N ) ) /\ N = [_ ( 1st ` t ) / s ]_ C ) -> j = ( 2nd ` t ) )
342 341 165 syl 
 |-  ( ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( 0 ... N ) ) /\ N = [_ ( 1st ` t ) / s ]_ C ) -> [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
343 eqtr 
 |-  ( ( N = [_ ( 1st ` t ) / s ]_ C /\ [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
344 343 ex 
 |-  ( N = [_ ( 1st ` t ) / s ]_ C -> ( [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
345 344 adantl 
 |-  ( ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( 0 ... N ) ) /\ N = [_ ( 1st ` t ) / s ]_ C ) -> ( [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
346 342 345 mpd 
 |-  ( ( ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) /\ j e. ( 0 ... N ) ) /\ N = [_ ( 1st ` t ) / s ]_ C ) -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
347 346 exp31 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( j e. ( 0 ... N ) -> ( N = [_ ( 1st ` t ) / s ]_ C -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) ) )
348 241 158 347 rexlimd 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
349 236 348 syl5 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( ( N e. ( 0 ... N ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
350 233 349 mpand 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
351 350 pm4.71rd 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) )
352 235 ralsng 
 |-  ( N e. NN -> ( A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C ) )
353 1 352 syl 
 |-  ( ph -> ( A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C ) )
354 353 ad2antrr 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( A. i e. { N } E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C ) )
355 230 351 354 3bitr3rd 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C <-> ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) )
356 355 notbid 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( -. E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C <-> -. ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) )
357 207 356 syl5bb 
 |-  ( ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C ) -> ( A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C <-> -. ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) )
358 357 pm5.32da 
 |-  ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) -> ( ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ -. ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) ) )
359 203 358 sylan2 
 |-  ( ( ph /\ t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ -. ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) ) )
360 359 rabbidva 
 |-  ( ph -> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C ) } = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ -. ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) } )
361 nfv 
 |-  F/ y t = <. x , k >.
362 nfv 
 |-  F/ y x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
363 nfrab1 
 |-  F/_ y { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) }
364 363 nfcri 
 |-  F/ y k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) }
365 362 364 nfan 
 |-  F/ y ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } )
366 361 365 nfan 
 |-  F/ y ( t = <. x , k >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
367 nfv 
 |-  F/ k ( t = <. x , y >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) )
368 opeq2 
 |-  ( k = y -> <. x , k >. = <. x , y >. )
369 368 eqeq2d 
 |-  ( k = y -> ( t = <. x , k >. <-> t = <. x , y >. ) )
370 eleq1 
 |-  ( k = y -> ( k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } <-> y e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
371 rabid 
 |-  ( y e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } <-> ( y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) )
372 370 371 bitrdi 
 |-  ( k = y -> ( k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } <-> ( y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) ) )
373 372 anbi2d 
 |-  ( k = y -> ( ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) <-> ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) ) ) )
374 3anass 
 |-  ( ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) <-> ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) ) )
375 373 374 bitr4di 
 |-  ( k = y -> ( ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) <-> ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) ) )
376 369 375 anbi12d 
 |-  ( k = y -> ( ( t = <. x , k >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) <-> ( t = <. x , y >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) ) ) )
377 366 367 376 cbvexv1 
 |-  ( E. k ( t = <. x , k >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) <-> E. y ( t = <. x , y >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) ) )
378 377 exbii 
 |-  ( E. x E. k ( t = <. x , k >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) <-> E. x E. y ( t = <. x , y >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) ) )
379 eliunxp 
 |-  ( t e. U_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) <-> E. x E. k ( t = <. x , k >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ k e. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) )
380 elopab 
 |-  ( t e. { <. x , y >. | ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) } <-> E. x E. y ( t = <. x , y >. /\ ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) ) )
381 378 379 380 3bitr4i 
 |-  ( t e. U_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) <-> t e. { <. x , y >. | ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) } )
382 381 eqriv 
 |-  U_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) = { <. x , y >. | ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) }
383 vex 
 |-  y e. _V
384 125 383 op2ndd 
 |-  ( t = <. x , y >. -> ( 2nd ` t ) = y )
385 384 sneqd 
 |-  ( t = <. x , y >. -> { ( 2nd ` t ) } = { y } )
386 385 difeq2d 
 |-  ( t = <. x , y >. -> ( ( 0 ... N ) \ { ( 2nd ` t ) } ) = ( ( 0 ... N ) \ { y } ) )
387 125 383 op1std 
 |-  ( t = <. x , y >. -> ( 1st ` t ) = x )
388 387 csbeq1d 
 |-  ( t = <. x , y >. -> [_ ( 1st ` t ) / s ]_ C = [_ x / s ]_ C )
389 388 eqeq2d 
 |-  ( t = <. x , y >. -> ( i = [_ ( 1st ` t ) / s ]_ C <-> i = [_ x / s ]_ C ) )
390 386 389 rexeqbidv 
 |-  ( t = <. x , y >. -> ( E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C ) )
391 390 ralbidv 
 |-  ( t = <. x , y >. -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C ) )
392 388 neeq2d 
 |-  ( t = <. x , y >. -> ( N =/= [_ ( 1st ` t ) / s ]_ C <-> N =/= [_ x / s ]_ C ) )
393 392 ralbidv 
 |-  ( t = <. x , y >. -> ( A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C <-> A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) )
394 391 393 anbi12d 
 |-  ( t = <. x , y >. -> ( ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) )
395 394 rabxp 
 |-  { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C ) } = { <. x , y >. | ( x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ y e. ( 0 ... N ) /\ ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) ) }
396 382 395 eqtr4i 
 |-  U_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C ) }
397 difrab 
 |-  ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } \ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C /\ -. ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) ) }
398 360 396 397 3eqtr4g 
 |-  ( ph -> U_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) = ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } \ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) )
399 398 fveq2d 
 |-  ( ph -> ( # ` U_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) = ( # ` ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } \ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) )
400 27 a1i 
 |-  ( ( ph /\ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) e. Fin )
401 inxp 
 |-  ( ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) i^i ( { t } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) = ( ( { x } i^i { t } ) X. ( { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } i^i { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) )
402 df-ne 
 |-  ( x =/= t <-> -. x = t )
403 disjsn2 
 |-  ( x =/= t -> ( { x } i^i { t } ) = (/) )
404 402 403 sylbir 
 |-  ( -. x = t -> ( { x } i^i { t } ) = (/) )
405 404 xpeq1d 
 |-  ( -. x = t -> ( ( { x } i^i { t } ) X. ( { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } i^i { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) = ( (/) X. ( { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } i^i { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) )
406 0xp 
 |-  ( (/) X. ( { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } i^i { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) = (/)
407 405 406 eqtrdi 
 |-  ( -. x = t -> ( ( { x } i^i { t } ) X. ( { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } i^i { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) = (/) )
408 401 407 syl5eq 
 |-  ( -. x = t -> ( ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) i^i ( { t } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) = (/) )
409 408 orri 
 |-  ( x = t \/ ( ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) i^i ( { t } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) = (/) )
410 409 rgen2w 
 |-  A. x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) A. t e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( x = t \/ ( ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) i^i ( { t } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) = (/) )
411 sneq 
 |-  ( x = t -> { x } = { t } )
412 csbeq1 
 |-  ( x = t -> [_ x / s ]_ C = [_ t / s ]_ C )
413 412 eqeq2d 
 |-  ( x = t -> ( i = [_ x / s ]_ C <-> i = [_ t / s ]_ C ) )
414 413 rexbidv 
 |-  ( x = t -> ( E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C ) )
415 414 ralbidv 
 |-  ( x = t -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C ) )
416 412 neeq2d 
 |-  ( x = t -> ( N =/= [_ x / s ]_ C <-> N =/= [_ t / s ]_ C ) )
417 416 ralbidv 
 |-  ( x = t -> ( A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C <-> A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) )
418 415 417 anbi12d 
 |-  ( x = t -> ( ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) ) )
419 418 rabbidv 
 |-  ( x = t -> { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } = { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } )
420 411 419 xpeq12d 
 |-  ( x = t -> ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) = ( { t } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) )
421 420 disjor 
 |-  ( Disj_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) <-> A. x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) A. t e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( x = t \/ ( ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) i^i ( { t } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ t / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ t / s ]_ C ) } ) ) = (/) ) )
422 410 421 mpbir 
 |-  Disj_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } )
423 422 a1i 
 |-  ( ph -> Disj_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) )
424 19 400 423 hashiun 
 |-  ( ph -> ( # ` U_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) = sum_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) )
425 399 424 eqtr3d 
 |-  ( ph -> ( # ` ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } \ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) = sum_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) )
426 fo1st 
 |-  1st : _V -onto-> _V
427 fofun 
 |-  ( 1st : _V -onto-> _V -> Fun 1st )
428 426 427 ax-mp 
 |-  Fun 1st
429 ssv 
 |-  { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } C_ _V
430 fof 
 |-  ( 1st : _V -onto-> _V -> 1st : _V --> _V )
431 426 430 ax-mp 
 |-  1st : _V --> _V
432 431 fdmi 
 |-  dom 1st = _V
433 429 432 sseqtrri 
 |-  { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } C_ dom 1st
434 fores 
 |-  ( ( Fun 1st /\ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } C_ dom 1st ) -> ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) )
435 428 433 434 mp2an 
 |-  ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } )
436 fveq2 
 |-  ( t = x -> ( 2nd ` t ) = ( 2nd ` x ) )
437 436 csbeq1d 
 |-  ( t = x -> [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
438 fveq2 
 |-  ( t = x -> ( 1st ` t ) = ( 1st ` x ) )
439 438 csbeq1d 
 |-  ( t = x -> [_ ( 1st ` t ) / s ]_ C = [_ ( 1st ` x ) / s ]_ C )
440 439 csbeq2dv 
 |-  ( t = x -> [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C )
441 437 440 eqtrd 
 |-  ( t = x -> [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C )
442 441 eqeq2d 
 |-  ( t = x -> ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C <-> N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) )
443 439 eqeq2d 
 |-  ( t = x -> ( i = [_ ( 1st ` t ) / s ]_ C <-> i = [_ ( 1st ` x ) / s ]_ C ) )
444 443 rexbidv 
 |-  ( t = x -> ( E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) )
445 444 ralbidv 
 |-  ( t = x -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) )
446 442 445 anbi12d 
 |-  ( t = x -> ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) <-> ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) )
447 446 rexrab 
 |-  ( E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = s <-> E. x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) )
448 xp1st 
 |-  ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` x ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
449 448 anim1i 
 |-  ( ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) -> ( ( 1st ` x ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) )
450 eleq1 
 |-  ( ( 1st ` x ) = s -> ( ( 1st ` x ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) <-> s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) )
451 csbeq1a 
 |-  ( s = ( 1st ` x ) -> C = [_ ( 1st ` x ) / s ]_ C )
452 451 eqcoms 
 |-  ( ( 1st ` x ) = s -> C = [_ ( 1st ` x ) / s ]_ C )
453 452 eqcomd 
 |-  ( ( 1st ` x ) = s -> [_ ( 1st ` x ) / s ]_ C = C )
454 453 eqeq2d 
 |-  ( ( 1st ` x ) = s -> ( i = [_ ( 1st ` x ) / s ]_ C <-> i = C ) )
455 454 rexbidv 
 |-  ( ( 1st ` x ) = s -> ( E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C <-> E. j e. ( 0 ... N ) i = C ) )
456 455 ralbidv 
 |-  ( ( 1st ` x ) = s -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C <-> A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) )
457 450 456 anbi12d 
 |-  ( ( 1st ` x ) = s -> ( ( ( 1st ` x ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) <-> ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) ) )
458 449 457 syl5ibcom 
 |-  ( ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) -> ( ( 1st ` x ) = s -> ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) ) )
459 458 adantrl 
 |-  ( ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) -> ( ( 1st ` x ) = s -> ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) ) )
460 459 expimpd 
 |-  ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) -> ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) ) )
461 460 rexlimiv 
 |-  ( E. x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) -> ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) )
462 simplr 
 |-  ( ( ( ph /\ s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
463 ovex 
 |-  ( 0 ... N ) e. _V
464 463 enref 
 |-  ( 0 ... N ) ~~ ( 0 ... N )
465 phpreu 
 |-  ( ( ( 0 ... N ) e. Fin /\ ( 0 ... N ) ~~ ( 0 ... N ) ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C <-> A. i e. ( 0 ... N ) E! j e. ( 0 ... N ) i = C ) )
466 23 464 465 mp2an 
 |-  ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C <-> A. i e. ( 0 ... N ) E! j e. ( 0 ... N ) i = C )
467 466 biimpi 
 |-  ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C -> A. i e. ( 0 ... N ) E! j e. ( 0 ... N ) i = C )
468 eqeq1 
 |-  ( i = N -> ( i = C <-> N = C ) )
469 468 reubidv 
 |-  ( i = N -> ( E! j e. ( 0 ... N ) i = C <-> E! j e. ( 0 ... N ) N = C ) )
470 469 rspcva 
 |-  ( ( N e. ( 0 ... N ) /\ A. i e. ( 0 ... N ) E! j e. ( 0 ... N ) i = C ) -> E! j e. ( 0 ... N ) N = C )
471 232 467 470 syl2an 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> E! j e. ( 0 ... N ) N = C )
472 riotacl 
 |-  ( E! j e. ( 0 ... N ) N = C -> ( iota_ j e. ( 0 ... N ) N = C ) e. ( 0 ... N ) )
473 471 472 syl 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> ( iota_ j e. ( 0 ... N ) N = C ) e. ( 0 ... N ) )
474 473 adantlr 
 |-  ( ( ( ph /\ s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> ( iota_ j e. ( 0 ... N ) N = C ) e. ( 0 ... N ) )
475 opelxpi 
 |-  ( ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( iota_ j e. ( 0 ... N ) N = C ) e. ( 0 ... N ) ) -> <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
476 462 474 475 syl2anc 
 |-  ( ( ( ph /\ s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
477 riotasbc 
 |-  ( E! j e. ( 0 ... N ) N = C -> [. ( iota_ j e. ( 0 ... N ) N = C ) / j ]. N = C )
478 471 477 syl 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> [. ( iota_ j e. ( 0 ... N ) N = C ) / j ]. N = C )
479 riotaex 
 |-  ( iota_ j e. ( 0 ... N ) N = C ) e. _V
480 sbceq2g 
 |-  ( ( iota_ j e. ( 0 ... N ) N = C ) e. _V -> ( [. ( iota_ j e. ( 0 ... N ) N = C ) / j ]. N = C <-> N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C ) )
481 479 480 ax-mp 
 |-  ( [. ( iota_ j e. ( 0 ... N ) N = C ) / j ]. N = C <-> N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C )
482 478 481 sylib 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C )
483 482 expcom 
 |-  ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C -> ( ph -> N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C ) )
484 483 imdistanri 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> ( N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) )
485 484 adantlr 
 |-  ( ( ( ph /\ s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> ( N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) )
486 vex 
 |-  s e. _V
487 486 479 op2ndd 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( 2nd ` x ) = ( iota_ j e. ( 0 ... N ) N = C ) )
488 487 csbeq1d 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> [_ ( 2nd ` x ) / j ]_ C = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C )
489 nfcv 
 |-  F/_ j s
490 nfriota1 
 |-  F/_ j ( iota_ j e. ( 0 ... N ) N = C )
491 489 490 nfop 
 |-  F/_ j <. s , ( iota_ j e. ( 0 ... N ) N = C ) >.
492 491 nfeq2 
 |-  F/ j x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >.
493 486 479 op1std 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( 1st ` x ) = s )
494 493 eqcomd 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> s = ( 1st ` x ) )
495 494 451 syl 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> C = [_ ( 1st ` x ) / s ]_ C )
496 492 495 csbeq2d 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> [_ ( 2nd ` x ) / j ]_ C = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C )
497 488 496 eqtr3d 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C )
498 497 eqeq2d 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C <-> N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) )
499 495 eqeq2d 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( i = C <-> i = [_ ( 1st ` x ) / s ]_ C ) )
500 492 499 rexbid 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( E. j e. ( 0 ... N ) i = C <-> E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) )
501 500 ralbidv 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C <-> A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) )
502 498 501 anbi12d 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( ( N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) <-> ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) )
503 493 biantrud 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) <-> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) ) )
504 502 503 bitr2d 
 |-  ( x = <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. -> ( ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) <-> ( N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) ) )
505 504 rspcev 
 |-  ( ( <. s , ( iota_ j e. ( 0 ... N ) N = C ) >. e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ ( N = [_ ( iota_ j e. ( 0 ... N ) N = C ) / j ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) ) -> E. x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) )
506 476 485 505 syl2anc 
 |-  ( ( ( ph /\ s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> E. x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) )
507 506 expl 
 |-  ( ph -> ( ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) -> E. x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) ) )
508 461 507 impbid2 
 |-  ( ph -> ( E. x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) /\ ( 1st ` x ) = s ) <-> ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) ) )
509 447 508 syl5bb 
 |-  ( ph -> ( E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = s <-> ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) ) )
510 509 abbidv 
 |-  ( ph -> { s | E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = s } = { s | ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) } )
511 dfimafn 
 |-  ( ( Fun 1st /\ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } C_ dom 1st ) -> ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = { y | E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = y } )
512 428 433 511 mp2an 
 |-  ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = { y | E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = y }
513 nfcv 
 |-  F/_ s ( 2nd ` t )
514 nfcsb1v 
 |-  F/_ s [_ ( 1st ` t ) / s ]_ C
515 513 514 nfcsbw 
 |-  F/_ s [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C
516 515 nfeq2 
 |-  F/ s N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C
517 nfcv 
 |-  F/_ s ( 0 ... N )
518 514 nfeq2 
 |-  F/ s i = [_ ( 1st ` t ) / s ]_ C
519 517 518 nfrex 
 |-  F/ s E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C
520 517 519 nfralw 
 |-  F/ s A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C
521 516 520 nfan 
 |-  F/ s ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C )
522 nfcv 
 |-  F/_ s ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) )
523 521 522 nfrabw 
 |-  F/_ s { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) }
524 nfv 
 |-  F/ s ( 1st ` x ) = y
525 523 524 nfrex 
 |-  F/ s E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = y
526 nfv 
 |-  F/ y E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = s
527 eqeq2 
 |-  ( y = s -> ( ( 1st ` x ) = y <-> ( 1st ` x ) = s ) )
528 527 rexbidv 
 |-  ( y = s -> ( E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = y <-> E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = s ) )
529 525 526 528 cbvabw 
 |-  { y | E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = y } = { s | E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = s }
530 512 529 eqtri 
 |-  ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = { s | E. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( 1st ` x ) = s }
531 df-rab 
 |-  { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } = { s | ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) }
532 510 530 531 3eqtr4g 
 |-  ( ph -> ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
533 foeq3 
 |-  ( ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } -> ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) <-> ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) )
534 532 533 syl 
 |-  ( ph -> ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> ( 1st " { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) <-> ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) )
535 435 534 mpbii 
 |-  ( ph -> ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
536 fof 
 |-  ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } -> ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } --> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
537 535 536 syl 
 |-  ( ph -> ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } --> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
538 fvres 
 |-  ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -> ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` x ) = ( 1st ` x ) )
539 fvres 
 |-  ( y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -> ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` y ) = ( 1st ` y ) )
540 538 539 eqeqan12d 
 |-  ( ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) -> ( ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` x ) = ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` y ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
541 540 adantl 
 |-  ( ( ph /\ ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) -> ( ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` x ) = ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` y ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
542 446 elrab 
 |-  ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } <-> ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) )
543 xp2nd 
 |-  ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 2nd ` x ) e. ( 0 ... N ) )
544 543 anim1i 
 |-  ( ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) -> ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) )
545 542 544 sylbi 
 |-  ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -> ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) )
546 simpl 
 |-  ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
547 546 a1i 
 |-  ( t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) -> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
548 547 ss2rabi 
 |-  { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } C_ { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C }
549 548 sseli 
 |-  ( y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -> y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C } )
550 fveq2 
 |-  ( t = y -> ( 2nd ` t ) = ( 2nd ` y ) )
551 550 csbeq1d 
 |-  ( t = y -> [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
552 fveq2 
 |-  ( t = y -> ( 1st ` t ) = ( 1st ` y ) )
553 552 csbeq1d 
 |-  ( t = y -> [_ ( 1st ` t ) / s ]_ C = [_ ( 1st ` y ) / s ]_ C )
554 553 csbeq2dv 
 |-  ( t = y -> [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C )
555 551 554 eqtrd 
 |-  ( t = y -> [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C )
556 555 eqeq2d 
 |-  ( t = y -> ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C <-> N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) )
557 556 elrab 
 |-  ( y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C } <-> ( y e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) )
558 xp2nd 
 |-  ( y e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 2nd ` y ) e. ( 0 ... N ) )
559 558 anim1i 
 |-  ( ( y e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) -> ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) )
560 557 559 sylbi 
 |-  ( y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C } -> ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) )
561 549 560 syl 
 |-  ( y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -> ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) )
562 545 561 anim12i 
 |-  ( ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) -> ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) )
563 an4 
 |-  ( ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) <-> ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) )
564 563 anbi2i 
 |-  ( ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) ) <-> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) ) )
565 anass 
 |-  ( ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) <-> ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) )
566 ancom 
 |-  ( ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) <-> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) ) )
567 565 566 bitr3i 
 |-  ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) <-> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) ) )
568 567 anbi1i 
 |-  ( ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) <-> ( ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) )
569 anass 
 |-  ( ( ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) <-> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) ) )
570 568 569 bitri 
 |-  ( ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) <-> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) ) )
571 anass 
 |-  ( ( ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) <-> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) ) )
572 564 570 571 3bitr4i 
 |-  ( ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) ) /\ ( ( 2nd ` y ) e. ( 0 ... N ) /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) <-> ( ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) )
573 562 572 sylib 
 |-  ( ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) -> ( ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) )
574 phpreu 
 |-  ( ( ( 0 ... N ) e. Fin /\ ( 0 ... N ) ~~ ( 0 ... N ) ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C <-> A. i e. ( 0 ... N ) E! j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) )
575 23 464 574 mp2an 
 |-  ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C <-> A. i e. ( 0 ... N ) E! j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C )
576 reurmo 
 |-  ( E! j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C -> E* j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C )
577 576 ralimi 
 |-  ( A. i e. ( 0 ... N ) E! j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C -> A. i e. ( 0 ... N ) E* j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C )
578 575 577 sylbi 
 |-  ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C -> A. i e. ( 0 ... N ) E* j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C )
579 eqeq1 
 |-  ( i = N -> ( i = [_ ( 1st ` x ) / s ]_ C <-> N = [_ ( 1st ` x ) / s ]_ C ) )
580 579 rmobidv 
 |-  ( i = N -> ( E* j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C <-> E* j e. ( 0 ... N ) N = [_ ( 1st ` x ) / s ]_ C ) )
581 580 rspcva 
 |-  ( ( N e. ( 0 ... N ) /\ A. i e. ( 0 ... N ) E* j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) -> E* j e. ( 0 ... N ) N = [_ ( 1st ` x ) / s ]_ C )
582 232 578 581 syl2an 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) -> E* j e. ( 0 ... N ) N = [_ ( 1st ` x ) / s ]_ C )
583 nfv 
 |-  F/ k N = [_ ( 1st ` x ) / s ]_ C
584 583 rmo3 
 |-  ( E* j e. ( 0 ... N ) N = [_ ( 1st ` x ) / s ]_ C <-> A. j e. ( 0 ... N ) A. k e. ( 0 ... N ) ( ( N = [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) -> j = k ) )
585 582 584 sylib 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) -> A. j e. ( 0 ... N ) A. k e. ( 0 ... N ) ( ( N = [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) -> j = k ) )
586 nfcsb1v 
 |-  F/_ j [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C
587 586 nfeq2 
 |-  F/ j N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C
588 nfs1v 
 |-  F/ j [ k / j ] N = [_ ( 1st ` x ) / s ]_ C
589 587 588 nfan 
 |-  F/ j ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C )
590 nfv 
 |-  F/ j ( 2nd ` x ) = k
591 589 590 nfim 
 |-  F/ j ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = k )
592 nfv 
 |-  F/ k ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = ( 2nd ` y ) )
593 csbeq1a 
 |-  ( j = ( 2nd ` x ) -> [_ ( 1st ` x ) / s ]_ C = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C )
594 593 eqeq2d 
 |-  ( j = ( 2nd ` x ) -> ( N = [_ ( 1st ` x ) / s ]_ C <-> N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) )
595 594 anbi1d 
 |-  ( j = ( 2nd ` x ) -> ( ( N = [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) <-> ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) ) )
596 eqeq1 
 |-  ( j = ( 2nd ` x ) -> ( j = k <-> ( 2nd ` x ) = k ) )
597 595 596 imbi12d 
 |-  ( j = ( 2nd ` x ) -> ( ( ( N = [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) -> j = k ) <-> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = k ) ) )
598 sbsbc 
 |-  ( [ k / j ] N = [_ ( 1st ` x ) / s ]_ C <-> [. k / j ]. N = [_ ( 1st ` x ) / s ]_ C )
599 vex 
 |-  k e. _V
600 sbceq2g 
 |-  ( k e. _V -> ( [. k / j ]. N = [_ ( 1st ` x ) / s ]_ C <-> N = [_ k / j ]_ [_ ( 1st ` x ) / s ]_ C ) )
601 599 600 ax-mp 
 |-  ( [. k / j ]. N = [_ ( 1st ` x ) / s ]_ C <-> N = [_ k / j ]_ [_ ( 1st ` x ) / s ]_ C )
602 598 601 bitri 
 |-  ( [ k / j ] N = [_ ( 1st ` x ) / s ]_ C <-> N = [_ k / j ]_ [_ ( 1st ` x ) / s ]_ C )
603 csbeq1 
 |-  ( k = ( 2nd ` y ) -> [_ k / j ]_ [_ ( 1st ` x ) / s ]_ C = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C )
604 603 eqeq2d 
 |-  ( k = ( 2nd ` y ) -> ( N = [_ k / j ]_ [_ ( 1st ` x ) / s ]_ C <-> N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) )
605 602 604 syl5bb 
 |-  ( k = ( 2nd ` y ) -> ( [ k / j ] N = [_ ( 1st ` x ) / s ]_ C <-> N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) )
606 605 anbi2d 
 |-  ( k = ( 2nd ` y ) -> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) <-> ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) ) )
607 eqeq2 
 |-  ( k = ( 2nd ` y ) -> ( ( 2nd ` x ) = k <-> ( 2nd ` x ) = ( 2nd ` y ) ) )
608 606 607 imbi12d 
 |-  ( k = ( 2nd ` y ) -> ( ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = k ) <-> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = ( 2nd ` y ) ) ) )
609 591 592 597 608 rspc2 
 |-  ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) -> ( A. j e. ( 0 ... N ) A. k e. ( 0 ... N ) ( ( N = [_ ( 1st ` x ) / s ]_ C /\ [ k / j ] N = [_ ( 1st ` x ) / s ]_ C ) -> j = k ) -> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = ( 2nd ` y ) ) ) )
610 585 609 syl5com 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C ) -> ( ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) -> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = ( 2nd ` y ) ) ) )
611 610 impr 
 |-  ( ( ph /\ ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) ) ) -> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = ( 2nd ` y ) ) )
612 csbeq1 
 |-  ( ( 1st ` x ) = ( 1st ` y ) -> [_ ( 1st ` x ) / s ]_ C = [_ ( 1st ` y ) / s ]_ C )
613 612 csbeq2dv 
 |-  ( ( 1st ` x ) = ( 1st ` y ) -> [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C )
614 613 eqeq2d 
 |-  ( ( 1st ` x ) = ( 1st ` y ) -> ( N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C <-> N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) )
615 614 anbi2d 
 |-  ( ( 1st ` x ) = ( 1st ` y ) -> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) <-> ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) )
616 615 imbi1d 
 |-  ( ( 1st ` x ) = ( 1st ` y ) -> ( ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` x ) / s ]_ C ) -> ( 2nd ` x ) = ( 2nd ` y ) ) <-> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) -> ( 2nd ` x ) = ( 2nd ` y ) ) ) )
617 611 616 syl5ibcom 
 |-  ( ( ph /\ ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) ) ) -> ( ( 1st ` x ) = ( 1st ` y ) -> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) -> ( 2nd ` x ) = ( 2nd ` y ) ) ) )
618 617 com23 
 |-  ( ( ph /\ ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) ) ) -> ( ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) -> ( ( 1st ` x ) = ( 1st ` y ) -> ( 2nd ` x ) = ( 2nd ` y ) ) ) )
619 618 impr 
 |-  ( ( ph /\ ( ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` x ) / s ]_ C /\ ( ( 2nd ` x ) e. ( 0 ... N ) /\ ( 2nd ` y ) e. ( 0 ... N ) ) ) /\ ( N = [_ ( 2nd ` x ) / j ]_ [_ ( 1st ` x ) / s ]_ C /\ N = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / s ]_ C ) ) ) -> ( ( 1st ` x ) = ( 1st ` y ) -> ( 2nd ` x ) = ( 2nd ` y ) ) )
620 573 619 sylan2 
 |-  ( ( ph /\ ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) -> ( ( 1st ` x ) = ( 1st ` y ) -> ( 2nd ` x ) = ( 2nd ` y ) ) )
621 elrabi 
 |-  ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -> x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
622 elrabi 
 |-  ( y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -> y e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
623 xpopth 
 |-  ( ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ y e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) <-> x = y ) )
624 623 biimpd 
 |-  ( ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ y e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) -> x = y ) )
625 624 expd 
 |-  ( ( x e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ y e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( 1st ` x ) = ( 1st ` y ) -> ( ( 2nd ` x ) = ( 2nd ` y ) -> x = y ) ) )
626 621 622 625 syl2an 
 |-  ( ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) -> ( ( 1st ` x ) = ( 1st ` y ) -> ( ( 2nd ` x ) = ( 2nd ` y ) -> x = y ) ) )
627 626 adantl 
 |-  ( ( ph /\ ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) -> ( ( 1st ` x ) = ( 1st ` y ) -> ( ( 2nd ` x ) = ( 2nd ` y ) -> x = y ) ) )
628 620 627 mpdd 
 |-  ( ( ph /\ ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) -> ( ( 1st ` x ) = ( 1st ` y ) -> x = y ) )
629 541 628 sylbid 
 |-  ( ( ph /\ ( x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } /\ y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) -> ( ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` x ) = ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` y ) -> x = y ) )
630 629 ralrimivva 
 |-  ( ph -> A. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } A. y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` x ) = ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` y ) -> x = y ) )
631 dff13 
 |-  ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -1-1-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } <-> ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } --> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } /\ A. x e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } A. y e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ( ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` x ) = ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ` y ) -> x = y ) ) )
632 537 630 631 sylanbrc 
 |-  ( ph -> ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -1-1-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
633 df-f1o 
 |-  ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -1-1-onto-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } <-> ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -1-1-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } /\ ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -onto-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) )
634 632 535 633 sylanbrc 
 |-  ( ph -> ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -1-1-onto-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
635 rabfi 
 |-  ( ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) e. Fin -> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } e. Fin )
636 138 635 ax-mp 
 |-  { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } e. Fin
637 636 elexi 
 |-  { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } e. _V
638 637 f1oen 
 |-  ( ( 1st |` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) : { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } -1-1-onto-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } -> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ~~ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
639 634 638 syl 
 |-  ( ph -> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ~~ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
640 rabfi 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. Fin -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } e. Fin )
641 136 640 ax-mp 
 |-  { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } e. Fin
642 hashen 
 |-  ( ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } e. Fin /\ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } e. Fin ) -> ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) <-> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ~~ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) )
643 636 641 642 mp2an 
 |-  ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) <-> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ~~ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
644 639 643 sylibr 
 |-  ( ph -> ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) )
645 644 oveq2d 
 |-  ( ph -> ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } ) - ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C ) } ) ) = ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) ) )
646 202 425 645 3eqtr3d 
 |-  ( ph -> sum_ x e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( # ` ( { x } X. { y e. ( 0 ... N ) | ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C /\ A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C ) } ) ) = ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) ) )
647 135 646 breqtrd 
 |-  ( ph -> 2 || ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) ) )