Theorem poimirlem26 32030

Description: Lemma for poimir 32037 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
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 } ) ) )

Distinct variable groups:   f, i, j, p, s, t   ph, j   j, N   ph, i, p, s, t   B, f, i, j, s, t   f, K, i, j, p, s, t   f, N, i, p, s, t   C, i, p, t

Allowed substitution hints:   ph( f)   B( p)   C( f, j, s)

Proof of Theorem poimirlem26

Dummy variables k x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzofi 12225	. . . . . 6 |- ( 0..^ K ) e. Fin
2		fzfi 12223	. . . . . 6 |- ( 1 ... N ) e. Fin
3		mapfi 7888	. . . . . 6 |- ( ( ( 0..^ K ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 0..^ K ) ^m ( 1 ... N ) ) e. Fin )
4	1, 2, 3	mp2an 686	. . . . 5 |- ( ( 0..^ K ) ^m ( 1 ... N ) ) e. Fin
5		mapfi 7888	. . . . . . 7 |- ( ( ( 1 ... N ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin )
6	2, 2, 5	mp2an 686	. . . . . 6 |- ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin
7		f1of 5828	. . . . . . . 8 |- ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> f : ( 1 ... N ) --> ( 1 ... N ) )
8	7	ss2abi 3487	. . . . . . 7 |- { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ { f | f : ( 1 ... N ) --> ( 1 ... N ) }
9		ovex 6336	. . . . . . . 8 |- ( 1 ... N ) e. _V
10	9, 9	mapval 7502	. . . . . . 7 |- ( ( 1 ... N ) ^m ( 1 ... N ) ) = { f | f : ( 1 ... N ) --> ( 1 ... N ) }
11	8, 10	sseqtr4i 3451	. . . . . 6 |- { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ ( ( 1 ... N ) ^m ( 1 ... N ) )
12		ssfi 7810	. . . . . 6 |- ( ( ( ( 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 )
13	6, 11, 12	mp2an 686	. . . . 5 |- { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin
14	4, 13	pm3.2i 462	. . . 4 |- ( ( ( 0..^ K ) ^m ( 1 ... N ) ) e. Fin /\ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin )
15		xpfi 7860	. . . 4 |- ( ( ( ( 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 )
16	14, 15	mp1i 13	. . 3 |- ( ph -> ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. Fin )
17		2z 10993	. . . 4 |- 2 e. ZZ
18	17	a1i 11	. . 3 |- ( ph -> 2 e. ZZ )
19		snfi 7668	. . . . . . 7 |- { x } e. Fin
20		fzfi 12223	. . . . . . . 8 |- ( 0 ... N ) e. Fin
21		rabfi 7814	. . . . . . . 8 |- ( ( 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 )
22	20, 21	ax-mp 5	. . . . . . 7 |- { 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
23		xpfi 7860	. . . . . . 7 |- ( ( { 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 )
24	19, 22, 23	mp2an 686	. . . . . 6 |- ( { 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
25		hashcl 12576	. . . . . 6 |- ( ( { 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 )
26	24, 25	ax-mp 5	. . . . 5 |- ( # ` ( { 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
27	26	nn0zi 10986	. . . 4 |- ( # ` ( { 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
28	27	a1i 11	. . 3 |- ( ( 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 )
29		poimir.0	. . . . . . . . . 10 |- ( ph -> N e. NN )
30	29	adantr 472	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> N e. NN )
31	30	adantr 472	. . . . . . . 8 |- ( ( ( 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 )
32		nfv 1769	. . . . . . . . . 10 |- F/ j p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) )
33		nfcsb1v 3365	. . . . . . . . . . 11 |- F/_ j [_ k / j ]_ [_ t / s ]_ C
34	33	nfeq2 2627	. . . . . . . . . 10 |- F/ j B = [_ k / j ]_ [_ t / s ]_ C
35	32, 34	nfim 2023	. . . . . . . . 9 |- 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 )
36		oveq2 6316	. . . . . . . . . . . . . . 15 |- ( j = k -> ( 1 ... j ) = ( 1 ... k ) )
37	36	imaeq2d 5174	. . . . . . . . . . . . . 14 |- ( j = k -> ( ( 2nd ` t ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... k ) ) )
38	37	xpeq1d 4862	. . . . . . . . . . . . 13 |- ( j = k -> ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) )
39		oveq1 6315	. . . . . . . . . . . . . . . 16 |- ( j = k -> ( j + 1 ) = ( k + 1 ) )
40	39	oveq1d 6323	. . . . . . . . . . . . . . 15 |- ( j = k -> ( ( j + 1 ) ... N ) = ( ( k + 1 ) ... N ) )
41	40	imaeq2d 5174	. . . . . . . . . . . . . 14 |- ( j = k -> ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) )
42	41	xpeq1d 4862	. . . . . . . . . . . . 13 |- ( j = k -> ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) )
43	38, 42	uneq12d 3580	. . . . . . . . . . . 12 |- ( 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 } ) ) )
44	43	oveq2d 6324	. . . . . . . . . . 11 |- ( 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 } ) ) ) )
45	44	eqeq2d 2481	. . . . . . . . . 10 |- ( 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 } ) ) ) ) )
46		csbeq1a 3358	. . . . . . . . . . 11 |- ( j = k -> [_ t / s ]_ C = [_ k / j ]_ [_ t / s ]_ C )
47	46	eqeq2d 2481	. . . . . . . . . 10 |- ( j = k -> ( B = [_ t / s ]_ C <-> B = [_ k / j ]_ [_ t / s ]_ C ) )
48	45, 47	imbi12d 327	. . . . . . . . 9 |- ( 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 ) ) )
49		nfv 1769	. . . . . . . . . . 11 |- F/ s p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
50		nfcsb1v 3365	. . . . . . . . . . . 12 |- F/_ s [_ t / s ]_ C
51	50	nfeq2 2627	. . . . . . . . . . 11 |- F/ s B = [_ t / s ]_ C
52	49, 51	nfim 2023	. . . . . . . . . 10 |- F/ s ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ t / s ]_ C )
53		fveq2 5879	. . . . . . . . . . . . 13 |- ( s = t -> ( 1st ` s ) = ( 1st ` t ) )
54		fveq2 5879	. . . . . . . . . . . . . . . 16 |- ( s = t -> ( 2nd ` s ) = ( 2nd ` t ) )
55	54	imaeq1d 5173	. . . . . . . . . . . . . . 15 |- ( s = t -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... j ) ) )
56	55	xpeq1d 4862	. . . . . . . . . . . . . 14 |- ( s = t -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) )
57	54	imaeq1d 5173	. . . . . . . . . . . . . . 15 |- ( s = t -> ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) )
58	57	xpeq1d 4862	. . . . . . . . . . . . . 14 |- ( s = t -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
59	56, 58	uneq12d 3580	. . . . . . . . . . . . 13 |- ( 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 } ) ) )
60	53, 59	oveq12d 6326	. . . . . . . . . . . 12 |- ( 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 } ) ) ) )
61	60	eqeq2d 2481	. . . . . . . . . . 11 |- ( 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 } ) ) ) ) )
62		csbeq1a 3358	. . . . . . . . . . . 12 |- ( s = t -> C = [_ t / s ]_ C )
63	62	eqeq2d 2481	. . . . . . . . . . 11 |- ( s = t -> ( B = C <-> B = [_ t / s ]_ C ) )
64	61, 63	imbi12d 327	. . . . . . . . . 10 |- ( 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 ) ) )
65		poimirlem28.1	. . . . . . . . . 10 |- ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
66	52, 64, 65	chvar 2119	. . . . . . . . 9 |- ( p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = [_ t / s ]_ C )
67	35, 48, 66	chvar 2119	. . . . . . . 8 |- ( 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		simpll 768	. . . . . . . . 9 |- ( ( ( 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 ) -> ph )
69		poimirlem28.2	. . . . . . . . 9 |- ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
70	68, 69	sylan 479	. . . . . . . 8 |- ( ( ( ( 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 ) )
71		xp1st 6842	. . . . . . . . . 10 |- ( 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 ) ) )
72		elmapi 7511	. . . . . . . . . 10 |- ( ( 1st ` x ) e. ( ( 0..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` x ) : ( 1 ... N ) --> ( 0..^ K ) )
73	71, 72	syl 17	. . . . . . . . 9 |- ( x e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` x ) : ( 1 ... N ) --> ( 0..^ K ) )
74	73	ad2antlr 741	. . . . . . . 8 |- ( ( ( 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 ) )
75		xp2nd 6843	. . . . . . . . . 10 |- ( 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 ) } )
76		fvex 5889	. . . . . . . . . . 11 |- ( 2nd ` x ) e. _V
77		f1oeq1 5818	. . . . . . . . . . 11 |- ( f = ( 2nd ` x ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` x ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
78	76, 77	elab 3173	. . . . . . . . . 10 |- ( ( 2nd ` x ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` x ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
79	75, 78	sylib 201	. . . . . . . . 9 |- ( 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 ) )
80	79	ad2antlr 741	. . . . . . . 8 |- ( ( ( 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 ) )
81		nfcv 2612	. . . . . . . . . . . . 13 |- F/_ j N
82		nfcv 2612	. . . . . . . . . . . . . 14 |- F/_ j x
83	82, 33	nfcsb 3367	. . . . . . . . . . . . 13 |- F/_ j [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
84	81, 83	nfne 2742	. . . . . . . . . . . 12 |- F/ j N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
85		nfcv 2612	. . . . . . . . . . . . . . 15 |- F/_ t C
86	85, 50, 62	cbvcsb 3354	. . . . . . . . . . . . . 14 |- [_ x / s ]_ C = [_ x / t ]_ [_ t / s ]_ C
87	46	csbeq2dv 3785	. . . . . . . . . . . . . 14 |- ( j = k -> [_ x / t ]_ [_ t / s ]_ C = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
88	86, 87	syl5eq 2517	. . . . . . . . . . . . 13 |- ( j = k -> [_ x / s ]_ C = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
89	88	neeq2d 2703	. . . . . . . . . . . 12 |- ( j = k -> ( N =/= [_ x / s ]_ C <-> N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
90	84, 89	rspc 3130	. . . . . . . . . . 11 |- ( k e. ( 0 ... N ) -> ( A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C -> N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
91	90	impcom 437	. . . . . . . . . 10 |- ( ( A. j e. ( 0 ... N ) N =/= [_ x / s ]_ C /\ k e. ( 0 ... N ) ) -> N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
92	91	adantll 728	. . . . . . . . 9 |- ( ( ( ( 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 )
93		1st2nd2 6849	. . . . . . . . . . 11 |- ( x e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
94	93	csbeq1d 3356	. . . . . . . . . 10 |- ( 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 )
95	94	ad3antlr 745	. . . . . . . . 9 |- ( ( ( ( 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 )
96	92, 95	neeqtrd 2712	. . . . . . . 8 |- ( ( ( ( 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 )
97	31, 67, 70, 74, 80, 96	poimirlem25 32029	. . . . . . 7 |- ( ( ( 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 } ) )
98		nfv 1769	. . . . . . . . . . . . . 14 |- F/ k i = [_ x / s ]_ C
99	83	nfeq2 2627	. . . . . . . . . . . . . 14 |- F/ j i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
100	88	eqeq2d 2481	. . . . . . . . . . . . . 14 |- ( j = k -> ( i = [_ x / s ]_ C <-> i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
101	98, 99, 100	cbvrex 3002	. . . . . . . . . . . . 13 |- ( E. j e. ( ( 0 ... N ) \ { y } ) i = [_ x / s ]_ C <-> E. k e. ( ( 0 ... N ) \ { y } ) i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
102	94	eqeq2d 2481	. . . . . . . . . . . . . 14 |- ( 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 ) )
103	102	rexbidv 2892	. . . . . . . . . . . . 13 |- ( 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 ) )
104	101, 103	syl5rbb 266	. . . . . . . . . . . 12 |- ( 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 ) )
105	104	ralbidv 2829	. . . . . . . . . . 11 |- ( 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 ) )
106		iba 511	. . . . . . . . . . 11 |- ( 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 ) ) )
107	105, 106	sylan9bb 714	. . . . . . . . . 10 |- ( ( 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 ) ) )
108	107	rabbidv 3022	. . . . . . . . 9 |- ( ( 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	108	fveq2d 5883	. . . . . . . 8 |- ( ( 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 ) } ) )
110	109	adantll 728	. . . . . . 7 |- ( ( ( 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 ) } ) )
111	97, 110	breqtrd 4420	. . . . . 6 |- ( ( ( 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 ) } ) )
112	111	ex 441	. . . . 5 |- ( ( 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 ) } ) ) )
113		dvds0 14395	. . . . . . . 8 |- ( 2 e. ZZ -> 2 || 0 )
114	17, 113	ax-mp 5	. . . . . . 7 |- 2 || 0
115		hash0 12586	. . . . . . 7 |- ( # ` (/) ) = 0
116	114, 115	breqtrri 4421	. . . . . 6 |- 2 || ( # ` (/) )
117		simpr 468	. . . . . . . . . 10 |- ( ( 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 )
118	117	con3i 142	. . . . . . . . 9 |- ( -. 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 ) )
119	118	ralrimivw 2810	. . . . . . . 8 |- ( -. 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 ) )
120		rabeq0 3757	. . . . . . . 8 |- ( { 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 ) )
121	119, 120	sylibr 217	. . . . . . 7 |- ( -. 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 ) } = (/) )
122	121	fveq2d 5883	. . . . . 6 |- ( -. 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 ) } ) = ( # ` (/) ) )
123	116, 122	syl5breqr 4432	. . . . 5 |- ( -. 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 ) } ) )
124	112, 123	pm2.61d1 164	. . . 4 |- ( ( 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 ) } ) )
125		hashxp 12647	. . . . . 6 |- ( ( { 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 ) } ) ) )
126	19, 22, 125	mp2an 686	. . . . 5 |- ( # ` ( { 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 ) } ) )
127		vex 3034	. . . . . . 7 |- x e. _V
128		hashsng 12587	. . . . . . 7 |- ( x e. _V -> ( # ` { x } ) = 1 )
129	127, 128	ax-mp 5	. . . . . 6 |- ( # ` { x } ) = 1
130	129	oveq1i 6318	. . . . 5 |- ( ( # ` { 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 ) } ) )
131		hashcl 12576	. . . . . . . 8 |- ( { 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 )
132	22, 131	ax-mp 5	. . . . . . 7 |- ( # ` { 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
133	132	nn0cni 10905	. . . . . 6 |- ( # ` { 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
134	133	mulid2i 9664	. . . . 5 |- ( 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 ) } )
135	126, 130, 134	3eqtri 2497	. . . 4 |- ( # ` ( { 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 ) } )
136	124, 135	syl6breqr 4436	. . 3 |- ( ( 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 ) } ) ) )
137	16, 18, 28, 136	fsumdvds 14425	. 2 |- ( 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 ) } ) ) )
138	4, 13, 15	mp2an 686	. . . . . 6 |- ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. Fin
139		xpfi 7860	. . . . . 6 |- ( ( ( ( ( 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 )
140	138, 20, 139	mp2an 686	. . . . 5 |- ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) e. Fin
141		rabfi 7814	. . . . 5 |- ( ( ( ( ( 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 )
142	140, 141	ax-mp 5	. . . 4 |- { 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
143	29	nncnd 10647	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
144		npcan1 10065	. . . . . . . . . . . 12 |- ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
145	143, 144	syl 17	. . . . . . . . . . 11 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
146		nnm1nn0 10935	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( N - 1 ) e. NN0 )
147	29, 146	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( N - 1 ) e. NN0 )
148	147	nn0zd 11061	. . . . . . . . . . . 12 |- ( ph -> ( N - 1 ) e. ZZ )
149		uzid 11197	. . . . . . . . . . . 12 |- ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
150		peano2uz 11235	. . . . . . . . . . . 12 |- ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
151	148, 149, 150	3syl 18	. . . . . . . . . . 11 |- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
152	145, 151	eqeltrrd 2550	. . . . . . . . . 10 |- ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
153		fzss2 11864	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
154		ssralv 3479	. . . . . . . . . 10 |- ( ( 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 ) )
155	152, 153, 154	3syl 18	. . . . . . . . 9 |- ( 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 ) )
156	155	adantr 472	. . . . . . . 8 |- ( ( 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 ) )
157		raldifb 3562	. . . . . . . . . . . 12 |- ( 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 )
158		nfv 1769	. . . . . . . . . . . . . . 15 |- F/ j ph
159		nfcsb1v 3365	. . . . . . . . . . . . . . . 16 |- F/_ j [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C
160	159	nfeq2 2627	. . . . . . . . . . . . . . 15 |- F/ j N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C
161	158, 160	nfan 2031	. . . . . . . . . . . . . 14 |- F/ j ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
162		nfv 1769	. . . . . . . . . . . . . 14 |- F/ j i e. ( 0 ... ( N - 1 ) )
163	161, 162	nfan 2031	. . . . . . . . . . . . 13 |- F/ j ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) )
164		nnel 2752	. . . . . . . . . . . . . . . . 17 |- ( -. j e/ { ( 2nd ` t ) } <-> j e. { ( 2nd ` t ) } )
165		elsn 3973	. . . . . . . . . . . . . . . . 17 |- ( j e. { ( 2nd ` t ) } <-> j = ( 2nd ` t ) )
166	164, 165	bitri 257	. . . . . . . . . . . . . . . 16 |- ( -. j e/ { ( 2nd ` t ) } <-> j = ( 2nd ` t ) )
167		csbeq1a 3358	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = ( 2nd ` t ) -> [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
168	167	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . 20 |- ( j = ( 2nd ` t ) -> ( N = [_ ( 1st ` t ) / s ]_ C <-> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
169	168	biimparc 495	. . . . . . . . . . . . . . . . . . 19 |- ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ j = ( 2nd ` t ) ) -> N = [_ ( 1st ` t ) / s ]_ C )
170	29	nnred 10646	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> N e. RR )
171	170	ltm1d 10561	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( N - 1 ) < N )
172	147	nn0red 10950	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( N - 1 ) e. RR )
173	172, 170	ltnled 9799	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
174	171, 173	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> -. N <_ ( N - 1 ) )
175		elfzle2 11829	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N e. ( 0 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
176	174, 175	nsyl 125	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> -. N e. ( 0 ... ( N - 1 ) ) )
177		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( i = N -> ( i e. ( 0 ... ( N - 1 ) ) <-> N e. ( 0 ... ( N - 1 ) ) ) )
178	177	notbid 301	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i = N -> ( -. i e. ( 0 ... ( N - 1 ) ) <-> -. N e. ( 0 ... ( N - 1 ) ) ) )
179	176, 178	syl5ibrcom 230	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( i = N -> -. i e. ( 0 ... ( N - 1 ) ) ) )
180	179	con2d 119	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( i e. ( 0 ... ( N - 1 ) ) -> -. i = N ) )
181	180	imp 436	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) -> -. i = N )
182		eqeq2 2482	. . . . . . . . . . . . . . . . . . . . 21 |- ( N = [_ ( 1st ` t ) / s ]_ C -> ( i = N <-> i = [_ ( 1st ` t ) / s ]_ C ) )
183	182	notbid 301	. . . . . . . . . . . . . . . . . . . 20 |- ( N = [_ ( 1st ` t ) / s ]_ C -> ( -. i = N <-> -. i = [_ ( 1st ` t ) / s ]_ C ) )
184	181, 183	syl5ibcom 228	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( N = [_ ( 1st ` t ) / s ]_ C -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
185	169, 184	syl5 32	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ j = ( 2nd ` t ) ) -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
186	185	expdimp 444	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) -> ( j = ( 2nd ` t ) -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
187	186	an32s 821	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( j = ( 2nd ` t ) -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
188	166, 187	syl5bi 225	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( -. j e/ { ( 2nd ` t ) } -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
189		idd 24	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( -. i = [_ ( 1st ` t ) / s ]_ C -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
190	188, 189	jad 167	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
191	190	adantr 472	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
192	163, 191	ralimdaa 2801	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
193	157, 192	syl5bir 226	. . . . . . . . . . 11 |- ( ( ( 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 ) )
194	193	con3d 140	. . . . . . . . . 10 |- ( ( ( 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 ) )
195		dfrex2 2837	. . . . . . . . . 10 |- ( E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> -. A. j e. ( 0 ... N ) -. i = [_ ( 1st ` t ) / s ]_ C )
196		dfrex2 2837	. . . . . . . . . 10 |- ( E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C <-> -. A. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) -. i = [_ ( 1st ` t ) / s ]_ C )
197	194, 195, 196	3imtr4g 278	. . . . . . . . 9 |- ( ( ( 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 ) )
198	197	ralimdva 2805	. . . . . . . 8 |- ( ( 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 ) )
199	156, 198	syld 44	. . . . . . 7 |- ( ( 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 ) )
200	199	expimpd 614	. . . . . 6 |- ( 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 ) )
201	200	adantr 472	. . . . 5 |- ( ( 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 ) )
202	201	ss2rabdv 3496	. . . 4 |- ( 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 } )
203		hashssdif 12627	. . . 4 |- ( ( { 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 ) } ) ) )
204	142, 202, 203	sylancr 676	. . 3 |- ( 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 ) } ) ) )
205		xp2nd 6843	. . . . . . . 8 |- ( 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 ) )
206		df-ne 2643	. . . . . . . . . . . 12 |- ( N =/= [_ ( 1st ` t ) / s ]_ C <-> -. N = [_ ( 1st ` t ) / s ]_ C )
207	206	ralbii 2823	. . . . . . . . . . 11 |- ( A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C <-> A. j e. ( 0 ... N ) -. N = [_ ( 1st ` t ) / s ]_ C )
208		ralnex 2834	. . . . . . . . . . 11 |- ( A. j e. ( 0 ... N ) -. N = [_ ( 1st ` t ) / s ]_ C <-> -. E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C )
209	207, 208	bitri 257	. . . . . . . . . 10 |- ( A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C <-> -. E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C )
210	29	nnnn0d 10949	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. NN0 )
211		nn0uz 11217	. . . . . . . . . . . . . . . . . . 19 |- NN0 = ( ZZ>= ` 0 )
212	210, 211	syl6eleq 2559	. . . . . . . . . . . . . . . . . 18 |- ( ph -> N e. ( ZZ>= ` 0 ) )
213	145, 212	eqeltrd 2549	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 0 ) )
214		fzsplit2 11850	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 0 ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
215	213, 152, 214	syl2anc 673	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
216	145	oveq1d 6323	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
217	29	nnzd 11062	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. ZZ )
218		fzsn 11866	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ZZ -> ( N ... N ) = { N } )
219	217, 218	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( N ... N ) = { N } )
220	216, 219	eqtrd 2505	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
221	220	uneq2d 3579	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( 0 ... ( N - 1 ) ) u. { N } ) )
222	215, 221	eqtrd 2505	. . . . . . . . . . . . . . 15 |- ( ph -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. { N } ) )
223	222	raleqdv 2979	. . . . . . . . . . . . . 14 |- ( 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 ) )
224		difss 3549	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 ... N ) \ { ( 2nd ` t ) } ) C_ ( 0 ... N )
225		ssrexv 3480	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
226	224, 225	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C -> E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C )
227	226	ralimi 2796	. . . . . . . . . . . . . . . 16 |- ( 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 )
228	227	biantrurd 516	. . . . . . . . . . . . . . 15 |- ( 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 ) ) )
229		ralunb 3606	. . . . . . . . . . . . . . 15 |- ( 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 ) )
230	228, 229	syl6rbbr 272	. . . . . . . . . . . . . 14 |- ( 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 ) )
231	223, 230	sylan9bb 714	. . . . . . . . . . . . 13 |- ( ( 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 ) )
232	231	adantlr 729	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
233		nn0fz0 11916	. . . . . . . . . . . . . . . 16 |- ( N e. NN0 <-> N e. ( 0 ... N ) )
234	210, 233	sylib 201	. . . . . . . . . . . . . . 15 |- ( ph -> N e. ( 0 ... N ) )
235	234	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
236		eqeq1 2475	. . . . . . . . . . . . . . . . 17 |- ( i = N -> ( i = [_ ( 1st ` t ) / s ]_ C <-> N = [_ ( 1st ` t ) / s ]_ C ) )
237	236	rexbidv 2892	. . . . . . . . . . . . . . . 16 |- ( i = N -> ( E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C ) )
238	237	rspcva 3134	. . . . . . . . . . . . . . 15 |- ( ( 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 )
239		nfv 1769	. . . . . . . . . . . . . . . . 17 |- F/ j ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) )
240		nfcv 2612	. . . . . . . . . . . . . . . . . 18 |- F/_ j ( 0 ... ( N - 1 ) )
241		nfre1 2846	. . . . . . . . . . . . . . . . . 18 |- F/ j E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C
242	240, 241	nfral 2789	. . . . . . . . . . . . . . . . 17 |- F/ j A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C
243	239, 242	nfan 2031	. . . . . . . . . . . . . . . 16 |- 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 )
244		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N = [_ ( 1st ` t ) / s ]_ C -> ( N e. ( 0 ... ( N - 1 ) ) <-> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
245	244	notbid 301	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( N = [_ ( 1st ` t ) / s ]_ C -> ( -. N e. ( 0 ... ( N - 1 ) ) <-> -. [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
246	176, 245	syl5ibcom 228	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( N = [_ ( 1st ` t ) / s ]_ C -> -. [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
247	246	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) ) ) )
248		eldifsn 4088	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) <-> ( j e. ( 0 ... N ) /\ j =/= ( 2nd ` t ) ) )
249		diffi 7821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 0 ... N ) e. Fin -> ( ( 0 ... N ) \ { ( 2nd ` t ) } ) e. Fin )
250	20, 249	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( 0 ... N ) \ { ( 2nd ` t ) } ) e. Fin
251		ssrab2 3500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } C_ ( ( 0 ... N ) \ { ( 2nd ` t ) } )
252		ssdomg 7633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( 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 ) } ) ) )
253	250, 251, 252	mp2 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } ~<_ ( ( 0 ... N ) \ { ( 2nd ` t ) } )
254		snssi 4107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( 2nd ` t ) e. ( 0 ... N ) -> { ( 2nd ` t ) } C_ ( 0 ... N ) )
255		hashssdif 12627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( 0 ... N ) e. Fin /\ { ( 2nd ` t ) } C_ ( 0 ... N ) ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( ( # ` ( 0 ... N ) ) - ( # ` { ( 2nd ` t ) } ) ) )
256	20, 254, 255	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 2nd ` t ) e. ( 0 ... N ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( ( # ` ( 0 ... N ) ) - ( # ` { ( 2nd ` t ) } ) ) )
257		ax-1cn 9615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- 1 e. CC
258		addsub 9906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( N e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = ( ( N - 1 ) + 1 ) )
259	257, 257, 258	mp3an23 1382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( N e. CC -> ( ( N + 1 ) - 1 ) = ( ( N - 1 ) + 1 ) )
260	143, 259	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> ( ( N + 1 ) - 1 ) = ( ( N - 1 ) + 1 ) )
261		hashfz0 12645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( N e. NN0 -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
262	210, 261	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
263		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 2nd ` t ) e. _V
264		hashsng 12587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( 2nd ` t ) e. _V -> ( # ` { ( 2nd ` t ) } ) = 1 )
265	263, 264	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> ( # ` { ( 2nd ` t ) } ) = 1 )
266	262, 265	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> ( ( # ` ( 0 ... N ) ) - ( # ` { ( 2nd ` t ) } ) ) = ( ( N + 1 ) - 1 ) )
267		hashfz0 12645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( N - 1 ) e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( ( N - 1 ) + 1 ) )
268	29, 146, 267	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( ( N - 1 ) + 1 ) )
269	260, 266, 268	3eqtr4d 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> ( ( # ` ( 0 ... N ) ) - ( # ` { ( 2nd ` t ) } ) ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
270	256, 269	sylan9eqr 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
271		fzfi 12223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 0 ... ( N - 1 ) ) e. Fin
272		hashen 12568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( 0 ... N ) \ { (