Theorem poimirlem26 31966

Description: Lemma for poimir 31973 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 12187	. . . . . 6 |- ( 0..^ K ) e. Fin
2		fzfi 12185	. . . . . 6 |- ( 1 ... N ) e. Fin
3		mapfi 7870	. . . . . 6 |- ( ( ( 0..^ K ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 0..^ K ) ^m ( 1 ... N ) ) e. Fin )
4	1, 2, 3	mp2an 678	. . . . 5 |- ( ( 0..^ K ) ^m ( 1 ... N ) ) e. Fin
5		mapfi 7870	. . . . . . 7 |- ( ( ( 1 ... N ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin )
6	2, 2, 5	mp2an 678	. . . . . 6 |- ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin
7		f1of 5814	. . . . . . . 8 |- ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> f : ( 1 ... N ) --> ( 1 ... N ) )
8	7	ss2abi 3501	. . . . . . 7 |- { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ { f | f : ( 1 ... N ) --> ( 1 ... N ) }
9		ovex 6318	. . . . . . . 8 |- ( 1 ... N ) e. _V
10	9, 9	mapval 7484	. . . . . . 7 |- ( ( 1 ... N ) ^m ( 1 ... N ) ) = { f | f : ( 1 ... N ) --> ( 1 ... N ) }
11	8, 10	sseqtr4i 3465	. . . . . 6 |- { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ ( ( 1 ... N ) ^m ( 1 ... N ) )
12		ssfi 7792	. . . . . 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 678	. . . . 5 |- { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin
14	4, 13	pm3.2i 457	. . . 4 |- ( ( ( 0..^ K ) ^m ( 1 ... N ) ) e. Fin /\ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin )
15		xpfi 7842	. . . 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 10969	. . . 4 |- 2 e. ZZ
18	17	a1i 11	. . 3 |- ( ph -> 2 e. ZZ )
19		snfi 7650	. . . . . . 7 |- { x } e. Fin
20		fzfi 12185	. . . . . . . 8 |- ( 0 ... N ) e. Fin
21		rabfi 7796	. . . . . . . 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 7842	. . . . . . 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 678	. . . . . 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 12538	. . . . . 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 10962	. . . 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 467	. . . . . . . . 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 467	. . . . . . . 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 1761	. . . . . . . . . 10 |- F/ j p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) ) )
33		nfcsb1v 3379	. . . . . . . . . . 11 |- F/_ j [_ k / j ]_ [_ t / s ]_ C
34	33	nfeq2 2607	. . . . . . . . . 10 |- F/ j B = [_ k / j ]_ [_ t / s ]_ C
35	32, 34	nfim 2003	. . . . . . . . 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 6298	. . . . . . . . . . . . . . 15 |- ( j = k -> ( 1 ... j ) = ( 1 ... k ) )
37	36	imaeq2d 5168	. . . . . . . . . . . . . 14 |- ( j = k -> ( ( 2nd ` t ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... k ) ) )
38	37	xpeq1d 4857	. . . . . . . . . . . . 13 |- ( j = k -> ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... k ) ) X. { 1 } ) )
39		oveq1 6297	. . . . . . . . . . . . . . . 16 |- ( j = k -> ( j + 1 ) = ( k + 1 ) )
40	39	oveq1d 6305	. . . . . . . . . . . . . . 15 |- ( j = k -> ( ( j + 1 ) ... N ) = ( ( k + 1 ) ... N ) )
41	40	imaeq2d 5168	. . . . . . . . . . . . . 14 |- ( j = k -> ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) )
42	41	xpeq1d 4857	. . . . . . . . . . . . 13 |- ( j = k -> ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( k + 1 ) ... N ) ) X. { 0 } ) )
43	38, 42	uneq12d 3589	. . . . . . . . . . . 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 6306	. . . . . . . . . . 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 2461	. . . . . . . . . 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 3372	. . . . . . . . . . 11 |- ( j = k -> [_ t / s ]_ C = [_ k / j ]_ [_ t / s ]_ C )
47	46	eqeq2d 2461	. . . . . . . . . 10 |- ( j = k -> ( B = [_ t / s ]_ C <-> B = [_ k / j ]_ [_ t / s ]_ C ) )
48	45, 47	imbi12d 322	. . . . . . . . 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 1761	. . . . . . . . . . 11 |- F/ s p = ( ( 1st ` t ) oF + ( ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
50		nfcsb1v 3379	. . . . . . . . . . . 12 |- F/_ s [_ t / s ]_ C
51	50	nfeq2 2607	. . . . . . . . . . 11 |- F/ s B = [_ t / s ]_ C
52	49, 51	nfim 2003	. . . . . . . . . 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 5865	. . . . . . . . . . . . 13 |- ( s = t -> ( 1st ` s ) = ( 1st ` t ) )
54		fveq2 5865	. . . . . . . . . . . . . . . 16 |- ( s = t -> ( 2nd ` s ) = ( 2nd ` t ) )
55	54	imaeq1d 5167	. . . . . . . . . . . . . . 15 |- ( s = t -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` t ) " ( 1 ... j ) ) )
56	55	xpeq1d 4857	. . . . . . . . . . . . . 14 |- ( s = t -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` t ) " ( 1 ... j ) ) X. { 1 } ) )
57	54	imaeq1d 5167	. . . . . . . . . . . . . . 15 |- ( s = t -> ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) )
58	57	xpeq1d 4857	. . . . . . . . . . . . . 14 |- ( s = t -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` t ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
59	56, 58	uneq12d 3589	. . . . . . . . . . . . 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 6308	. . . . . . . . . . . 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 2461	. . . . . . . . . . 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 3372	. . . . . . . . . . . 12 |- ( s = t -> C = [_ t / s ]_ C )
63	62	eqeq2d 2461	. . . . . . . . . . 11 |- ( s = t -> ( B = C <-> B = [_ t / s ]_ C ) )
64	61, 63	imbi12d 322	. . . . . . . . . 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 2106	. . . . . . . . 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 2106	. . . . . . . 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 760	. . . . . . . . 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 474	. . . . . . . 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 6823	. . . . . . . . . 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 7493	. . . . . . . . . 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 733	. . . . . . . 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 6824	. . . . . . . . . 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 5875	. . . . . . . . . . 11 |- ( 2nd ` x ) e. _V
77		f1oeq1 5805	. . . . . . . . . . 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 3185	. . . . . . . . . 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 200	. . . . . . . . 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 733	. . . . . . . 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 2592	. . . . . . . . . . . . 13 |- F/_ j N
82		nfcv 2592	. . . . . . . . . . . . . 14 |- F/_ j x
83	82, 33	nfcsb 3381	. . . . . . . . . . . . 13 |- F/_ j [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
84	81, 83	nfne 2723	. . . . . . . . . . . 12 |- F/ j N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
85		nfcv 2592	. . . . . . . . . . . . . . 15 |- F/_ t C
86	85, 50, 62	cbvcsb 3368	. . . . . . . . . . . . . 14 |- [_ x / s ]_ C = [_ x / t ]_ [_ t / s ]_ C
87	46	csbeq2dv 3781	. . . . . . . . . . . . . 14 |- ( j = k -> [_ x / t ]_ [_ t / s ]_ C = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
88	86, 87	syl5eq 2497	. . . . . . . . . . . . 13 |- ( j = k -> [_ x / s ]_ C = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C )
89	88	neeq2d 2684	. . . . . . . . . . . 12 |- ( j = k -> ( N =/= [_ x / s ]_ C <-> N =/= [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
90	84, 89	rspc 3144	. . . . . . . . . . 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 432	. . . . . . . . . 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 720	. . . . . . . . 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 6830	. . . . . . . . . . 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 3370	. . . . . . . . . 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 737	. . . . . . . . 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 2693	. . . . . . . 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 31965	. . . . . . 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 1761	. . . . . . . . . . . . . 14 |- F/ k i = [_ x / s ]_ C
99	83	nfeq2 2607	. . . . . . . . . . . . . 14 |- F/ j i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C
100	88	eqeq2d 2461	. . . . . . . . . . . . . 14 |- ( j = k -> ( i = [_ x / s ]_ C <-> i = [_ x / t ]_ [_ k / j ]_ [_ t / s ]_ C ) )
101	98, 99, 100	cbvrex 3016	. . . . . . . . . . . . 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 2461	. . . . . . . . . . . . . 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 2901	. . . . . . . . . . . . 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 262	. . . . . . . . . . . 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 2827	. . . . . . . . . . 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 506	. . . . . . . . . . 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 706	. . . . . . . . . 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 3036	. . . . . . . . 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 5869	. . . . . . . 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 720	. . . . . . 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 4427	. . . . . 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 436	. . . . 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 14318	. . . . . . . 8 |- ( 2 e. ZZ -> 2 || 0 )
114	17, 113	ax-mp 5	. . . . . . 7 |- 2 || 0
115		hash0 12548	. . . . . . 7 |- ( # ` (/) ) = 0
116	114, 115	breqtrri 4428	. . . . . 6 |- 2 || ( # ` (/) )
117		simpr 463	. . . . . . . . . 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 141	. . . . . . . . 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 2803	. . . . . . . 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 3754	. . . . . . . 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 216	. . . . . . 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 5869	. . . . . 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 4439	. . . . 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 163	. . . 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 12606	. . . . . 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 678	. . . . 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 3048	. . . . . . 7 |- x e. _V
128		hashsng 12549	. . . . . . 7 |- ( x e. _V -> ( # ` { x } ) = 1 )
129	127, 128	ax-mp 5	. . . . . 6 |- ( # ` { x } ) = 1
130	129	oveq1i 6300	. . . . 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 12538	. . . . . . . 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 10881	. . . . . 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 9646	. . . . 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 2477	. . . 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 4443	. . 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 14348	. 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 678	. . . . . 6 |- ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. Fin
139		xpfi 7842	. . . . . 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 678	. . . . 5 |- ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) e. Fin
141		rabfi 7796	. . . . 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 10625	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
144		npcan1 10044	. . . . . . . . . . . 12 |- ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
145	143, 144	syl 17	. . . . . . . . . . 11 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
146		nnm1nn0 10911	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( N - 1 ) e. NN0 )
147	29, 146	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( N - 1 ) e. NN0 )
148	147	nn0zd 11038	. . . . . . . . . . . 12 |- ( ph -> ( N - 1 ) e. ZZ )
149		uzid 11173	. . . . . . . . . . . 12 |- ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
150		peano2uz 11212	. . . . . . . . . . . 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 2530	. . . . . . . . . 10 |- ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
153		fzss2 11838	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
154		ssralv 3493	. . . . . . . . . 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 467	. . . . . . . 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 3573	. . . . . . . . . . . 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 1761	. . . . . . . . . . . . . . 15 |- F/ j ph
159		nfcsb1v 3379	. . . . . . . . . . . . . . . 16 |- F/_ j [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C
160	159	nfeq2 2607	. . . . . . . . . . . . . . 15 |- F/ j N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C
161	158, 160	nfan 2011	. . . . . . . . . . . . . 14 |- F/ j ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
162		nfv 1761	. . . . . . . . . . . . . 14 |- F/ j i e. ( 0 ... ( N - 1 ) )
163	161, 162	nfan 2011	. . . . . . . . . . . . 13 |- F/ j ( ( ph /\ N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) /\ i e. ( 0 ... ( N - 1 ) ) )
164		nnel 2733	. . . . . . . . . . . . . . . . 17 |- ( -. j e/ { ( 2nd ` t ) } <-> j e. { ( 2nd ` t ) } )
165		elsn 3982	. . . . . . . . . . . . . . . . 17 |- ( j e. { ( 2nd ` t ) } <-> j = ( 2nd ` t ) )
166	164, 165	bitri 253	. . . . . . . . . . . . . . . 16 |- ( -. j e/ { ( 2nd ` t ) } <-> j = ( 2nd ` t ) )
167		csbeq1a 3372	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = ( 2nd ` t ) -> [_ ( 1st ` t ) / s ]_ C = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C )
168	167	eqeq2d 2461	. . . . . . . . . . . . . . . . . . . 20 |- ( j = ( 2nd ` t ) -> ( N = [_ ( 1st ` t ) / s ]_ C <-> N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C ) )
169	168	biimparc 490	. . . . . . . . . . . . . . . . . . 19 |- ( ( N = [_ ( 2nd ` t ) / j ]_ [_ ( 1st ` t ) / s ]_ C /\ j = ( 2nd ` t ) ) -> N = [_ ( 1st ` t ) / s ]_ C )
170	29	nnred 10624	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> N e. RR )
171	170	ltm1d 10539	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( N - 1 ) < N )
172	147	nn0red 10926	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( N - 1 ) e. RR )
173	172, 170	ltnled 9782	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
174	171, 173	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> -. N <_ ( N - 1 ) )
175		elfzle2 11803	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N e. ( 0 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
176	174, 175	nsyl 125	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> -. N e. ( 0 ... ( N - 1 ) ) )
177		eleq1 2517	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( i = N -> ( i e. ( 0 ... ( N - 1 ) ) <-> N e. ( 0 ... ( N - 1 ) ) ) )
178	177	notbid 296	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i = N -> ( -. i e. ( 0 ... ( N - 1 ) ) <-> -. N e. ( 0 ... ( N - 1 ) ) ) )
179	176, 178	syl5ibrcom 226	. . . . . . . . . . . . . . . . . . . . . 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 431	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) -> -. i = N )
182		eqeq2 2462	. . . . . . . . . . . . . . . . . . . . 21 |- ( N = [_ ( 1st ` t ) / s ]_ C -> ( i = N <-> i = [_ ( 1st ` t ) / s ]_ C ) )
183	182	notbid 296	. . . . . . . . . . . . . . . . . . . 20 |- ( N = [_ ( 1st ` t ) / s ]_ C -> ( -. i = N <-> -. i = [_ ( 1st ` t ) / s ]_ C ) )
184	181, 183	syl5ibcom 224	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0 ... ( N - 1 ) ) ) -> ( N = [_ ( 1st ` t ) / s ]_ C -> -. i = [_ ( 1st ` t ) / s ]_ C ) )
185	169, 184	syl5 33	. . . . . . . . . . . . . . . . . 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 439	. . . . . . . . . . . . . . . . 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 813	. . . . . . . . . . . . . . . 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 221	. . . . . . . . . . . . . . 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 25	. . . . . . . . . . . . . . 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 166	. . . . . . . . . . . . . 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 467	. . . . . . . . . . . . 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 2790	. . . . . . . . . . . 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 222	. . . . . . . . . . 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 139	. . . . . . . . . 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 2838	. . . . . . . . . 10 |- ( E. j e. ( 0 ... N ) i = [_ ( 1st ` t ) / s ]_ C <-> -. A. j e. ( 0 ... N ) -. i = [_ ( 1st ` t ) / s ]_ C )
196		dfrex2 2838	. . . . . . . . . 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 274	. . . . . . . . 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 2796	. . . . . . . 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 45	. . . . . . 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 608	. . . . . 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 467	. . . . 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 3510	. . . 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 12588	. . . 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 669	. . 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 6824	. . . . . . . 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 2624	. . . . . . . . . . . 12 |- ( N =/= [_ ( 1st ` t ) / s ]_ C <-> -. N = [_ ( 1st ` t ) / s ]_ C )
207	206	ralbii 2819	. . . . . . . . . . 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 253	. . . . . . . . . 10 |- ( A. j e. ( 0 ... N ) N =/= [_ ( 1st ` t ) / s ]_ C <-> -. E. j e. ( 0 ... N ) N = [_ ( 1st ` t ) / s ]_ C )
210	29	nnnn0d 10925	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. NN0 )
211		nn0uz 11193	. . . . . . . . . . . . . . . . . . 19 |- NN0 = ( ZZ>= ` 0 )
212	210, 211	syl6eleq 2539	. . . . . . . . . . . . . . . . . 18 |- ( ph -> N e. ( ZZ>= ` 0 ) )
213	145, 212	eqeltrd 2529	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 0 ) )
214		fzsplit2 11824	. . . . . . . . . . . . . . . . 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 667	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
216	145	oveq1d 6305	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
217	29	nnzd 11039	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. ZZ )
218		fzsn 11840	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ZZ -> ( N ... N ) = { N } )
219	217, 218	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( N ... N ) = { N } )
220	216, 219	eqtrd 2485	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
221	220	uneq2d 3588	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 0 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( 0 ... ( N - 1 ) ) u. { N } ) )
222	215, 221	eqtrd 2485	. . . . . . . . . . . . . . 15 |- ( ph -> ( 0 ... N ) = ( ( 0 ... ( N - 1 ) ) u. { N } ) )
223	222	raleqdv 2993	. . . . . . . . . . . . . 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 3560	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 ... N ) \ { ( 2nd ` t ) } ) C_ ( 0 ... N )
225		ssrexv 3494	. . . . . . . . . . . . . . . . . 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 2781	. . . . . . . . . . . . . . . 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 511	. . . . . . . . . . . . . . 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 3615	. . . . . . . . . . . . . . 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 268	. . . . . . . . . . . . . 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 706	. . . . . . . . . . . . 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 721	. . . . . . . . . . . 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 11890	. . . . . . . . . . . . . . . 16 |- ( N e. NN0 <-> N e. ( 0 ... N ) )
234	210, 233	sylib 200	. . . . . . . . . . . . . . 15 |- ( ph -> N e. ( 0 ... N ) )
235	234	ad2antrr 732	. . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . . . . . 17 |- ( i = N -> ( i = [_ ( 1st ` t ) / s ]_ C <-> N = [_ ( 1st ` t ) / s ]_ C ) )
237	236	rexbidv 2901	. . . . . . . . . . . . . . . 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 3148	. . . . . . . . . . . . . . 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 1761	. . . . . . . . . . . . . . . . 17 |- F/ j ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) )
240		nfcv 2592	. . . . . . . . . . . . . . . . . 18 |- F/_ j ( 0 ... ( N - 1 ) )
241		nfre1 2848	. . . . . . . . . . . . . . . . . 18 |- F/ j E. j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ C
242	240, 241	nfral 2774	. . . . . . . . . . . . . . . . 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 2011	. . . . . . . . . . . . . . . 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 2517	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N = [_ ( 1st ` t ) / s ]_ C -> ( N e. ( 0 ... ( N - 1 ) ) <-> [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
245	244	notbid 296	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( N = [_ ( 1st ` t ) / s ]_ C -> ( -. N e. ( 0 ... ( N - 1 ) ) <-> -. [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
246	176, 245	syl5ibcom 224	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( N = [_ ( 1st ` t ) / s ]_ C -> -. [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
247	246	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . 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 4097	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) <-> ( j e. ( 0 ... N ) /\ j =/= ( 2nd ` t ) ) )
249		diffi 7803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- { j e. ( ( 0 ... N ) \ { ( 2nd ` t ) } ) | [_ ( 1st ` t ) / s ]_ C e. ( 0 ... ( N - 1 ) ) } C_ ( ( 0 ... N ) \ { ( 2nd ` t ) } )
252		ssdomg 7615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( 2nd ` t ) e. ( 0 ... N ) -> { ( 2nd ` t ) } C_ ( 0 ... N ) )
255		hashssdif 12588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( 0 ... N ) e. Fin /\ { ( 2nd ` t ) } C_ ( 0 ... N ) ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( ( # ` ( 0 ... N ) ) - ( # ` { ( 2nd ` t ) } ) ) )
256	20, 254, 255	sylancr 669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 2nd ` t ) e. ( 0 ... N ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( ( # ` ( 0 ... N ) ) - ( # ` { ( 2nd ` t ) } ) ) )
257		ax-1cn 9597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- 1 e. CC
258		addsub 9886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( N e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = ( ( N - 1 ) + 1 ) )
259	257, 257, 258	mp3an23 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( N e. NN0 -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
262	210, 261	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
263		fvex 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 2nd ` t ) e. _V
264		hashsng 12549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( 2nd ` t ) e. _V -> ( # ` { ( 2nd ` t ) } ) = 1 )
265	263, 264	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> ( # ` { ( 2nd ` t ) } ) = 1 )
266	262, 265	oveq12d 6308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> ( ( # ` ( 0 ... N ) ) - ( # ` { ( 2nd ` t ) } ) ) = ( ( N + 1 ) - 1 ) )
267		hashfz0 12604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> ( ( # ` ( 0 ... N ) ) - ( # ` { ( 2nd ` t ) } ) ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
270	256, 269	sylan9eqr 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( 2nd ` t ) e. ( 0 ... N ) ) -> ( # ` ( ( 0 ... N ) \ { ( 2nd ` t ) } ) ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
271		fzfi 12185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 0 ... ( N - 1 ) ) e. Fin
272		hashen 12530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( 0 ... N ) \ { (