Theorem poimirlem24 32028

Description: Lemma for poimir 32037, two ways of expressing that a simplex has an admissible face on the back face of the cube. (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 ) )
poimirlem25.3	|- ( ph -> T : ( 1 ... N ) --> ( 0..^ K ) )
poimirlem25.4	|- ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem24.5	|- ( ph -> V e. ( 0 ... N ) )

Assertion

Ref

Expression

poimirlem24

|- ( ph -> ( E. x e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) /\ ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C /\ -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) ) )

Distinct variable groups:   i, j, p, s, x, y, ph   j, N, y   T, j, y   U, j, y   j, V, y   ph, i, p, s   B, i, j, s   i, K, j, p, s   i, N, p, s   T, i, p   U, i, p   T, s   ph, x   x, B, y   C, i, p, x, y   x, K, y   x, N   x, T   U, s, x   i, V, p, s, x

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

Proof of Theorem poimirlem24

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1769	. . . . . . . . 9 |- F/ j ( ph /\ y e. ( 0 ... ( N - 1 ) ) )
2		nfcsb1v 3365	. . . . . . . . . 10 |- F/_ j [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
3		nfcv 2612	. . . . . . . . . 10 |- F/_ j ( 1 ... N )
4		nfcv 2612	. . . . . . . . . 10 |- F/_ j ( 0 ... K )
5	2, 3, 4	nff 5735	. . . . . . . . 9 |- F/ j [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K )
6	1, 5	nfim 2023	. . . . . . . 8 |- F/ j ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
7		eleq1 2537	. . . . . . . . . 10 |- ( j = y -> ( j e. ( 0 ... ( N - 1 ) ) <-> y e. ( 0 ... ( N - 1 ) ) ) )
8	7	anbi2d 718	. . . . . . . . 9 |- ( j = y -> ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) <-> ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) ) )
9		csbeq1a 3358	. . . . . . . . . 10 |- ( j = y -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
10	9	feq1d 5724	. . . . . . . . 9 |- ( j = y -> ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) <-> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
11	8, 10	imbi12d 327	. . . . . . . 8 |- ( j = y -> ( ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) <-> ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) ) )
12		poimir.0	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN )
13	12	nncnd 10647	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
14		npcan1 10065	. . . . . . . . . . . . 13 |- ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
15	13, 14	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
16	12	nnzd 11062	. . . . . . . . . . . . . 14 |- ( ph -> N e. ZZ )
17		peano2zm 11004	. . . . . . . . . . . . . 14 |- ( N e. ZZ -> ( N - 1 ) e. ZZ )
18	16, 17	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( N - 1 ) e. ZZ )
19		uzid 11197	. . . . . . . . . . . . 13 |- ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
20		peano2uz 11235	. . . . . . . . . . . . 13 |- ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
21	18, 19, 20	3syl 18	. . . . . . . . . . . 12 |- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
22	15, 21	eqeltrrd 2550	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
23		fzss2 11864	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
24	22, 23	syl 17	. . . . . . . . . 10 |- ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
25	24	sselda 3418	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> j e. ( 0 ... N ) )
26		elun 3565	. . . . . . . . . . . . 13 |- ( y e. ( { 1 } u. { 0 } ) <-> ( y e. { 1 } \/ y e. { 0 } ) )
27		fzofzp1 12037	. . . . . . . . . . . . . . 15 |- ( x e. ( 0..^ K ) -> ( x + 1 ) e. ( 0 ... K ) )
28		elsni 3985	. . . . . . . . . . . . . . . . 17 |- ( y e. { 1 } -> y = 1 )
29	28	oveq2d 6324	. . . . . . . . . . . . . . . 16 |- ( y e. { 1 } -> ( x + y ) = ( x + 1 ) )
30	29	eleq1d 2533	. . . . . . . . . . . . . . 15 |- ( y e. { 1 } -> ( ( x + y ) e. ( 0 ... K ) <-> ( x + 1 ) e. ( 0 ... K ) ) )
31	27, 30	syl5ibrcom 230	. . . . . . . . . . . . . 14 |- ( x e. ( 0..^ K ) -> ( y e. { 1 } -> ( x + y ) e. ( 0 ... K ) ) )
32		elfzoelz 11947	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( 0..^ K ) -> x e. ZZ )
33	32	zcnd 11064	. . . . . . . . . . . . . . . . 17 |- ( x e. ( 0..^ K ) -> x e. CC )
34	33	addid1d 9851	. . . . . . . . . . . . . . . 16 |- ( x e. ( 0..^ K ) -> ( x + 0 ) = x )
35		elfzofz 11962	. . . . . . . . . . . . . . . 16 |- ( x e. ( 0..^ K ) -> x e. ( 0 ... K ) )
36	34, 35	eqeltrd 2549	. . . . . . . . . . . . . . 15 |- ( x e. ( 0..^ K ) -> ( x + 0 ) e. ( 0 ... K ) )
37		elsni 3985	. . . . . . . . . . . . . . . . 17 |- ( y e. { 0 } -> y = 0 )
38	37	oveq2d 6324	. . . . . . . . . . . . . . . 16 |- ( y e. { 0 } -> ( x + y ) = ( x + 0 ) )
39	38	eleq1d 2533	. . . . . . . . . . . . . . 15 |- ( y e. { 0 } -> ( ( x + y ) e. ( 0 ... K ) <-> ( x + 0 ) e. ( 0 ... K ) ) )
40	36, 39	syl5ibrcom 230	. . . . . . . . . . . . . 14 |- ( x e. ( 0..^ K ) -> ( y e. { 0 } -> ( x + y ) e. ( 0 ... K ) ) )
41	31, 40	jaod 387	. . . . . . . . . . . . 13 |- ( x e. ( 0..^ K ) -> ( ( y e. { 1 } \/ y e. { 0 } ) -> ( x + y ) e. ( 0 ... K ) ) )
42	26, 41	syl5bi 225	. . . . . . . . . . . 12 |- ( x e. ( 0..^ K ) -> ( y e. ( { 1 } u. { 0 } ) -> ( x + y ) e. ( 0 ... K ) ) )
43	42	imp 436	. . . . . . . . . . 11 |- ( ( x e. ( 0..^ K ) /\ y e. ( { 1 } u. { 0 } ) ) -> ( x + y ) e. ( 0 ... K ) )
44	43	adantl 473	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. ( 0..^ K ) /\ y e. ( { 1 } u. { 0 } ) ) ) -> ( x + y ) e. ( 0 ... K ) )
45		poimirlem25.3	. . . . . . . . . . 11 |- ( ph -> T : ( 1 ... N ) --> ( 0..^ K ) )
46	45	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... N ) ) -> T : ( 1 ... N ) --> ( 0..^ K ) )
47		1ex 9656	. . . . . . . . . . . . . 14 |- 1 e. _V
48	47	fconst 5782	. . . . . . . . . . . . 13 |- ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 }
49		c0ex 9655	. . . . . . . . . . . . . 14 |- 0 e. _V
50	49	fconst 5782	. . . . . . . . . . . . 13 |- ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 }
51	48, 50	pm3.2i 462	. . . . . . . . . . . 12 |- ( ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 } /\ ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 } )
52		poimirlem25.4	. . . . . . . . . . . . . 14 |- ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
53		dff1o3 5834	. . . . . . . . . . . . . . 15 |- ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( U : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' U ) )
54	53	simprbi 471	. . . . . . . . . . . . . 14 |- ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' U )
55		imain 5669	. . . . . . . . . . . . . 14 |- ( Fun `' U -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) )
56	52, 54, 55	3syl 18	. . . . . . . . . . . . 13 |- ( ph -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) )
57		elfznn0 11913	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( 0 ... N ) -> j e. NN0 )
58	57	nn0red 10950	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... N ) -> j e. RR )
59	58	ltp1d 10559	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... N ) -> j < ( j + 1 ) )
60		fzdisj 11852	. . . . . . . . . . . . . . . 16 |- ( j < ( j + 1 ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... N ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
62	61	imaeq2d 5174	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... N ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( U " (/) ) )
63		ima0 5189	. . . . . . . . . . . . . 14 |- ( U " (/) ) = (/)
64	62, 63	syl6eq 2521	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... N ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = (/) )
65	56, 64	sylan9req 2526	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) )
66		fun 5758	. . . . . . . . . . . 12 |- ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 } /\ ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 } ) /\ ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
67	51, 65, 66	sylancr 676	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
68		nn0p1nn 10933	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN0 -> ( j + 1 ) e. NN )
69	57, 68	syl 17	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... N ) -> ( j + 1 ) e. NN )
70		nnuz 11218	. . . . . . . . . . . . . . . . 17 |- NN = ( ZZ>= ` 1 )
71	69, 70	syl6eleq 2559	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... N ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
72		elfzuz3 11823	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... N ) -> N e. ( ZZ>= ` j ) )
73		fzsplit2 11850	. . . . . . . . . . . . . . . 16 |- ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` j ) ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
74	71, 72, 73	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... N ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
75	74	imaeq2d 5174	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... N ) -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) )
76		imaundi 5254	. . . . . . . . . . . . . 14 |- ( U " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) )
77	75, 76	syl6req 2522	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... N ) -> ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) = ( U " ( 1 ... N ) ) )
78		f1ofo 5835	. . . . . . . . . . . . . 14 |- ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) -onto-> ( 1 ... N ) )
79		foima 5811	. . . . . . . . . . . . . 14 |- ( U : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
80	52, 78, 79	3syl 18	. . . . . . . . . . . . 13 |- ( ph -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
81	77, 80	sylan9eqr 2527	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
82	81	feq2d 5725	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) <-> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) ) )
83	67, 82	mpbid 215	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) )
84		ovex 6336	. . . . . . . . . . 11 |- ( 1 ... N ) e. _V
85	84	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( 1 ... N ) e. _V )
86		inidm 3632	. . . . . . . . . 10 |- ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
87	44, 46, 83, 85, 85, 86	off 6565	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
88	25, 87	syldan 478	. . . . . . . 8 |- ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
89	6, 11, 88	chvar 2119	. . . . . . 7 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
90		fzp1elp1 11875	. . . . . . . . 9 |- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) )
91	15	oveq2d 6324	. . . . . . . . . . 11 |- ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
92	91	eleq2d 2534	. . . . . . . . . 10 |- ( ph -> ( ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) <-> ( y + 1 ) e. ( 0 ... N ) ) )
93	92	biimpa 492	. . . . . . . . 9 |- ( ( ph /\ ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) ) -> ( y + 1 ) e. ( 0 ... N ) )
94	90, 93	sylan2 482	. . . . . . . 8 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y + 1 ) e. ( 0 ... N ) )
95		nfv 1769	. . . . . . . . . 10 |- F/ j ( ph /\ ( y + 1 ) e. ( 0 ... N ) )
96		nfcsb1v 3365	. . . . . . . . . . 11 |- F/_ j [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
97	96, 3, 4	nff 5735	. . . . . . . . . 10 |- F/ j [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K )
98	95, 97	nfim 2023	. . . . . . . . 9 |- F/ j ( ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
99		ovex 6336	. . . . . . . . 9 |- ( y + 1 ) e. _V
100		eleq1 2537	. . . . . . . . . . 11 |- ( j = ( y + 1 ) -> ( j e. ( 0 ... N ) <-> ( y + 1 ) e. ( 0 ... N ) ) )
101	100	anbi2d 718	. . . . . . . . . 10 |- ( j = ( y + 1 ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) ) )
102		csbeq1a 3358	. . . . . . . . . . 11 |- ( j = ( y + 1 ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
103	102	feq1d 5724	. . . . . . . . . 10 |- ( j = ( y + 1 ) -> ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) <-> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
104	101, 103	imbi12d 327	. . . . . . . . 9 |- ( j = ( y + 1 ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) <-> ( ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) ) )
105	98, 99, 104, 87	vtoclf 3085	. . . . . . . 8 |- ( ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
106	94, 105	syldan 478	. . . . . . 7 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
107		csbeq1 3352	. . . . . . . . 9 |- ( y = if ( y < V , y , ( y + 1 ) ) -> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
108	107	feq1d 5724	. . . . . . . 8 |- ( y = if ( y < V , y , ( y + 1 ) ) -> ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) <-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
109		csbeq1 3352	. . . . . . . . 9 |- ( ( y + 1 ) = if ( y < V , y , ( y + 1 ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
110	109	feq1d 5724	. . . . . . . 8 |- ( ( y + 1 ) = if ( y < V , y , ( y + 1 ) ) -> ( [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) <-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
111	108, 110	ifboth 3908	. . . . . . 7 |- ( ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
112	89, 106, 111	syl2anc 673	. . . . . 6 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
113		ovex 6336	. . . . . . 7 |- ( 0 ... K ) e. _V
114	113, 84	elmap 7518	. . . . . 6 |- ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. ( ( 0 ... K ) ^m ( 1 ... N ) ) <-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
115	112, 114	sylibr 217	. . . . 5 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. ( ( 0 ... K ) ^m ( 1 ... N ) ) )
116		eqid 2471	. . . . 5 |- ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
117	115, 116	fmptd 6061	. . . 4 |- ( ph -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
118		ovex 6336	. . . . 5 |- ( ( 0 ... K ) ^m ( 1 ... N ) ) e. _V
119		ovex 6336	. . . . 5 |- ( 0 ... ( N - 1 ) ) e. _V
120	118, 119	elmap 7518	. . . 4 |- ( ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) <-> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
121	117, 120	sylibr 217	. . 3 |- ( ph -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) )
122		rneq 5066	. . . . . . . 8 |- ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ran x = ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
123	122	mpteq1d 4477	. . . . . . 7 |- ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( p e. ran x |-> B ) = ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) )
124	123	rneqd 5068	. . . . . 6 |- ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ran ( p e. ran x |-> B ) = ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) )
125	124	sseq2d 3446	. . . . 5 |- ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) <-> ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) ) )
126	122	rexeqdv 2980	. . . . 5 |- ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( E. p e. ran x ( p ` N ) =/= 0 <-> E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) )
127	125, 126	anbi12d 725	. . . 4 |- ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) <-> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) ) )
128	127	ceqsrexv 3160	. . 3 |- ( ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) -> ( E. x e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) /\ ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) ) <-> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) ) )
129	121, 128	syl 17	. 2 |- ( ph -> ( E. x e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) /\ ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) ) <-> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) ) )
130		dfss3 3408	. . . 4 |- ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> A. i e. ( 0 ... ( N - 1 ) ) i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) )
131		ovex 6336	. . . . . . . . . . . . 13 |- ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
132		poimirlem28.1	. . . . . . . . . . . . 13 |- ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
133	131, 132	csbie 3375	. . . . . . . . . . . 12 |- [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = C
134	133	csbeq2i 3786	. . . . . . . . . . 11 |- [_ <. T , U >. / s ]_ [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ <. T , U >. / s ]_ C
135		opex 4664	. . . . . . . . . . . . 13 |- <. T , U >. e. _V
136	135	a1i 11	. . . . . . . . . . . 12 |- ( ph -> <. T , U >. e. _V )
137		fveq2 5879	. . . . . . . . . . . . . . 15 |- ( s = <. T , U >. -> ( 1st ` s ) = ( 1st ` <. T , U >. ) )
138		fex 6155	. . . . . . . . . . . . . . . . 17 |- ( ( T : ( 1 ... N ) --> ( 0..^ K ) /\ ( 1 ... N ) e. _V ) -> T e. _V )
139	45, 84, 138	sylancl 675	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. _V )
140		f1oexrnex 6761	. . . . . . . . . . . . . . . . 17 |- ( ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( 1 ... N ) e. _V ) -> U e. _V )
141	52, 84, 140	sylancl 675	. . . . . . . . . . . . . . . 16 |- ( ph -> U e. _V )
142		op1stg 6824	. . . . . . . . . . . . . . . 16 |- ( ( T e. _V /\ U e. _V ) -> ( 1st ` <. T , U >. ) = T )
143	139, 141, 142	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1st ` <. T , U >. ) = T )
144	137, 143	sylan9eqr 2527	. . . . . . . . . . . . . 14 |- ( ( ph /\ s = <. T , U >. ) -> ( 1st ` s ) = T )
145		fveq2 5879	. . . . . . . . . . . . . . . 16 |- ( s = <. T , U >. -> ( 2nd ` s ) = ( 2nd ` <. T , U >. ) )
146		op2ndg 6825	. . . . . . . . . . . . . . . . 17 |- ( ( T e. _V /\ U e. _V ) -> ( 2nd ` <. T , U >. ) = U )
147	139, 141, 146	syl2anc 673	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2nd ` <. T , U >. ) = U )
148	145, 147	sylan9eqr 2527	. . . . . . . . . . . . . . 15 |- ( ( ph /\ s = <. T , U >. ) -> ( 2nd ` s ) = U )
149		imaeq1 5169	. . . . . . . . . . . . . . . . 17 |- ( ( 2nd ` s ) = U -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( U " ( 1 ... j ) ) )
150	149	xpeq1d 4862	. . . . . . . . . . . . . . . 16 |- ( ( 2nd ` s ) = U -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... j ) ) X. { 1 } ) )
151		imaeq1 5169	. . . . . . . . . . . . . . . . 17 |- ( ( 2nd ` s ) = U -> ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) = ( U " ( ( j + 1 ) ... N ) ) )
152	151	xpeq1d 4862	. . . . . . . . . . . . . . . 16 |- ( ( 2nd ` s ) = U -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
153	150, 152	uneq12d 3580	. . . . . . . . . . . . . . 15 |- ( ( 2nd ` s ) = U -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
154	148, 153	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ s = <. T , U >. ) -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
155	144, 154	oveq12d 6326	. . . . . . . . . . . . 13 |- ( ( ph /\ s = <. T , U >. ) -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
156	155	csbeq1d 3356	. . . . . . . . . . . 12 |- ( ( ph /\ s = <. T , U >. ) -> [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
157	136, 156	csbied 3376	. . . . . . . . . . 11 |- ( ph -> [_ <. T , U >. / s ]_ [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
158	134, 157	syl5eqr 2519	. . . . . . . . . 10 |- ( ph -> [_ <. T , U >. / s ]_ C = [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
159	158	csbeq2dv 3785	. . . . . . . . 9 |- ( ph -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
160	159	eqeq2d 2481	. . . . . . . 8 |- ( ph -> ( i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B ) )
161	160	rexbidv 2892	. . . . . . 7 |- ( ph -> ( E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B ) )
162		vex 3034	. . . . . . . . 9 |- i e. _V
163		eqid 2471	. . . . . . . . . 10 |- ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) = ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B )
164	163	elrnmpt 5087	. . . . . . . . 9 |- ( i e. _V -> ( i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = B ) )
165	162, 164	ax-mp 5	. . . . . . . 8 |- ( i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = B )
166		nfv 1769	. . . . . . . . 9 |- F/ k i = B
167		nfcsb1v 3365	. . . . . . . . . 10 |- F/_ p [_ k / p ]_ B
168	167	nfeq2 2627	. . . . . . . . 9 |- F/ p i = [_ k / p ]_ B
169		csbeq1a 3358	. . . . . . . . . 10 |- ( p = k -> B = [_ k / p ]_ B )
170	169	eqeq2d 2481	. . . . . . . . 9 |- ( p = k -> ( i = B <-> i = [_ k / p ]_ B ) )
171	166, 168, 170	cbvrex 3002	. . . . . . . 8 |- ( E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = B <-> E. k e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = [_ k / p ]_ B )
172		ovex 6336	. . . . . . . . . . 11 |- ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
173	172	csbex 4531	. . . . . . . . . 10 |- [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
174	173	rgenw 2768	. . . . . . . . 9 |- A. y e. ( 0 ... ( N - 1 ) ) [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
175		csbeq1 3352	. . . . . . . . . . . 12 |- ( k = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> [_ k / p ]_ B = [_ [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
176		vex 3034	. . . . . . . . . . . . . 14 |- y e. _V
177	176, 99	ifex 3940	. . . . . . . . . . . . 13 |- if ( y < V , y , ( y + 1 ) ) e. _V
178		csbnestg 3791	. . . . . . . . . . . . 13 |- ( if ( y < V , y , ( y + 1 ) ) e. _V -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
179	177, 178	ax-mp 5	. . . . . . . . . . . 12 |- [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B
180	175, 179	syl6eqr 2523	. . . . . . . . . . 11 |- ( k = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> [_ k / p ]_ B = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
181	180	eqeq2d 2481	. . . . . . . . . 10 |- ( k = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( i = [_ k / p ]_ B <-> i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B ) )
182	116, 181	rexrnmpt 6047	. . . . . . . . 9 |- ( A. y e. ( 0 ... ( N - 1 ) ) [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V -> ( E. k e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = [_ k / p ]_ B <-> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B ) )
183	174, 182	ax-mp 5	. . . . . . . 8 |- ( E. k e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = [_ k / p ]_ B <-> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
184	165, 171, 183	3bitri 279	. . . . . . 7 |- ( i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
185	161, 184	syl6bbr 271	. . . . . 6 |- ( ph -> ( E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) ) )
186	24	sselda 3418	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. ( 0 ... N ) )
187	186	adantr 472	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y e. ( 0 ... N ) )
188		elfzelz 11826	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ... ( N - 1 ) ) -> y e. ZZ )
189	188	zred 11063	. . . . . . . . . . . . 13 |- ( y e. ( 0 ... ( N - 1 ) ) -> y e. RR )
190	189	adantl 473	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. RR )
191		ltne 9748	. . . . . . . . . . . . 13 |- ( ( y e. RR /\ y < V ) -> V =/= y )
192	191	necomd 2698	. . . . . . . . . . . 12 |- ( ( y e. RR /\ y < V ) -> y =/= V )
193	190, 192	sylan 479	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y =/= V )
194		eldifsn 4088	. . . . . . . . . . 11 |- ( y e. ( ( 0 ... N ) \ { V } ) <-> ( y e. ( 0 ... N ) /\ y =/= V ) )
195	187, 193, 194	sylanbrc 677	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y e. ( ( 0 ... N ) \ { V } ) )
196	94	adantr 472	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) e. ( 0 ... N ) )
197		poimirlem24.5	. . . . . . . . . . . . . . 15 |- ( ph -> V e. ( 0 ... N ) )
198		elfzelz 11826	. . . . . . . . . . . . . . 15 |- ( V e. ( 0 ... N ) -> V e. ZZ )
199	197, 198	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> V e. ZZ )
200	199	zred 11063	. . . . . . . . . . . . 13 |- ( ph -> V e. RR )
201	200	ad2antrr 740	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> V e. RR )
202		zre 10965	. . . . . . . . . . . . . . . 16 |- ( V e. ZZ -> V e. RR )
203		zre 10965	. . . . . . . . . . . . . . . 16 |- ( y e. ZZ -> y e. RR )
204		lenlt 9730	. . . . . . . . . . . . . . . 16 |- ( ( V e. RR /\ y e. RR ) -> ( V <_ y <-> -. y < V ) )
205	202, 203, 204	syl2an 485	. . . . . . . . . . . . . . 15 |- ( ( V e. ZZ /\ y e. ZZ ) -> ( V <_ y <-> -. y < V ) )
206		zleltp1 11011	. . . . . . . . . . . . . . 15 |- ( ( V e. ZZ /\ y e. ZZ ) -> ( V <_ y <-> V < ( y + 1 ) ) )
207	205, 206	bitr3d 263	. . . . . . . . . . . . . 14 |- ( ( V e. ZZ /\ y e. ZZ ) -> ( -. y < V <-> V < ( y + 1 ) ) )
208	199, 188, 207	syl2an 485	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( -. y < V <-> V < ( y + 1 ) ) )
209	208	biimpa 492	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> V < ( y + 1 ) )
210	201, 209	gtned 9787	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) =/= V )
211		eldifsn 4088	. . . . . . . . . . 11 |- ( ( y + 1 ) e. ( ( 0 ... N ) \ { V } ) <-> ( ( y + 1 ) e. ( 0 ... N ) /\ ( y + 1 ) =/= V ) )
212	196, 210, 211	sylanbrc 677	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) e. ( ( 0 ... N ) \ { V } ) )
213	195, 212	ifclda 3904	. . . . . . . . 9 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < V , y , ( y + 1 ) ) e. ( ( 0 ... N ) \ { V } ) )
214		nfcsb1v 3365	. . . . . . . . . . . 12 |- F/_ j [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
215	214	nfeq2 2627	. . . . . . . . . . 11 |- F/ j i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
216		csbeq1a 3358	. . . . . . . . . . . 12 |- ( j = if ( y < V , y , ( y + 1 ) ) -> [_ <. T , U >. / s ]_ C = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
217	216	eqeq2d 2481	. . . . . . . . . . 11 |- ( j = if ( y < V , y , ( y + 1 ) ) -> ( i = [_ <. T , U >. / s ]_ C <-> i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
218	215, 217	rspce 3131	. . . . . . . . . 10 |- ( ( if ( y < V , y , ( y + 1 ) ) e. ( ( 0 ... N ) \ { V } ) /\ i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) -> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C )
219	218	ex 441	. . . . . . . . 9 |- ( if ( y < V , y , ( y + 1 ) ) e. ( ( 0 ... N ) \ { V } ) -> ( i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C -> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
220	213, 219	syl 17	. . . . . . . 8 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C -> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
221	220	rexlimdva 2871	. . . . . . 7 |- ( ph -> ( E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C -> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
222		nfv 1769	. . . . . . . 8 |- F/ j ph
223		nfcv 2612	. . . . . . . . 9 |- F/_ j ( 0 ... ( N - 1 ) )
224	223, 215	nfrex 2848	. . . . . . . 8 |- F/ j E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
225		eldifi 3544	. . . . . . . . . . . . . . 15 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j e. ( 0 ... N ) )
226	225, 57	syl 17	. . . . . . . . . . . . . 14 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j e. NN0 )
227	226	nn0ge0d 10952	. . . . . . . . . . . . 13 |- ( j e. ( ( 0 ... N ) \ { V } ) -> 0 <_ j )
228	227	ad2antlr 741	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> 0 <_ j )
229	226	nn0red 10950	. . . . . . . . . . . . . . 15 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j e. RR )
230	229	ad2antlr 741	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j e. RR )
231	200	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> V e. RR )
232	16	zred 11063	. . . . . . . . . . . . . . 15 |- ( ph -> N e. RR )
233	232	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> N e. RR )
234		simpr 468	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j < V )
235		elfzle2 11829	. . . . . . . . . . . . . . . 16 |- ( V e. ( 0 ... N ) -> V <_ N )
236	197, 235	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> V <_ N )
237	236	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> V <_ N )
238	230, 231, 233, 234, 237	ltletrd 9812	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j < N )
239	226	nn0zd 11061	. . . . . . . . . . . . . . 15 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j e. ZZ )
240		zltlem1 11013	. . . . . . . . . . . . . . 15 |- ( ( j e. ZZ /\ N e. ZZ ) -> ( j < N <-> j <_ ( N - 1 ) ) )
241	239, 16, 240	syl2anr 486	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j < N <-> j <_ ( N - 1 ) ) )
242	241	adantr 472	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> ( j < N <-> j <_ ( N - 1 ) ) )
243	238, 242	mpbid 215	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j <_ ( N - 1 ) )
244		0z 10972	. . . . . . . . . . . . . . 15 |- 0 e. ZZ
245		elfz 11816	. . . . . . . . . . . . . . 15 |- ( ( j e. ZZ /\ 0 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
246	244, 245	mp3an2 1378	. . . . . . . . . . . . . 14 |- ( ( j e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
247	239, 18, 246	syl2anr 486	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
248	247	adantr 472	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
249	228, 243, 248	mpbir2and 936	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j e. ( 0 ... ( N - 1 ) ) )
250		0red 9662	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 e. RR )
251	200	ad2antrr 740	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V e. RR )
252	229	ad2antlr 741	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j e. RR )
253		elfzle1 11828	. . . . . . . . . . . . . . . . 17 |- ( V e. ( 0 ... N ) -> 0 <_ V )
254	197, 253	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ V )
255	254	ad2antrr 740	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 <_ V )
256		lenlt 9730	. . . . . . . . . . . . . . . . . 18 |- ( ( V e. RR /\ j e. RR ) -> ( V <_ j <-> -. j < V ) )
257	200, 229, 256	syl2an 485	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( V <_ j <-> -. j < V ) )
258	257	biimpar 493	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V <_ j )
259		eldifsni 4089	. . . . . . . . . . . . . . . . 17 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j =/= V )
260	259	ad2antlr 741	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j =/= V )
261		ltlen 9753	. . . . . . . . . . . . . . . . . 18 |- ( ( V e. RR /\ j e. RR ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
262	200, 229, 261	syl2an 485	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
263	262	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
264	258, 260, 263	mpbir2and 936	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V < j )
265	250, 251, 252, 255, 264	lelttrd 9810	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 < j )
266		zgt0ge1 11014	. . . . . . . . . . . . . . . 16 |- ( j e. ZZ -> ( 0 < j <-> 1 <_ j ) )
267	239, 266	syl 17	. . . . . . . . . . . . . . 15 |- ( j e. ( ( 0 ... N ) \ { V } ) -> ( 0 < j <-> 1 <_ j ) )
268	267	ad2antlr 741	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( 0 < j <-> 1 <_ j ) )
269	265, 268	mpbid 215	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 1 <_ j )
270		elfzle2 11829	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... N ) -> j <_ N )
271	225, 270	syl 17	. . . . . . . . . . . . . 14 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j <_ N )
272	271	ad2antlr 741	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j <_ N )
273		1z 10991	. . . . . . . . . . . . . . . 16 |- 1 e. ZZ
274		elfz 11816	. . . . . . . . . . . . . . . 16 |- ( ( j e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
275	273, 274	mp3an2 1378	. . . . . . . . . . . . . . 15 |- ( ( j e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
276	239, 16, 275	syl2anr 486	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
277	276	adantr 472	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
278	269, 272, 277	mpbir2and 936	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j e. ( 1 ... N ) )
279		elfzmlbm 11926	. . . . . . . . . . . 12 |- ( j e. ( 1 ... N ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
280	278, 279	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
281	249, 280	ifclda 3904	. . . . . . . . . 10 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> if ( j < V , j , ( j - 1 ) ) e. ( 0 ... ( N - 1 ) ) )
282		breq1 4398	. . . . . . . . . . . . . . . 16 |- ( j = if ( j < V , j , ( j - 1 ) ) -> ( j < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
283		id 22	. . . . . . . . . . . . . . . 16 |- ( j = if ( j < V , j , ( j - 1 ) ) -> j = if ( j < V , j , ( j - 1 ) ) )
284		oveq1 6315	. . . . . . . . . . . . . . . 16 |- ( j = if ( j < V , j , ( j - 1 ) ) -> ( j + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
285	282, 283, 284	ifbieq12d 3899	. . . . . . . . . . . . . . 15 |- ( j = if ( j < V , j , ( j - 1 ) ) -> if ( j < V , j , ( j + 1 ) ) = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) )
286	285	eqeq2d 2481	. . . . . . . . . . . . . 14 |- ( j = if ( j < V , j , ( j - 1 ) ) -> ( j = if ( j < V , j , ( j + 1 ) ) <-> j = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) ) )
287		breq1 4398	. . . . . . . . . . . . . . . 16 |- ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( ( j - 1 ) < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
288		id 22	. . . . . . . . . . . . . . . 16 |- ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) )
289		oveq1 6315	. . . . . . . . . . . . . . . 16 |- ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( ( j - 1 ) + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
290	287, 288, 289	ifbieq12d 3899	. . . . . . . . . . . . . . 15 |- ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) )
291	290	eqeq2d 2481	. . . . . . . . . . . . . 14 |- ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( j = if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) <-> j = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) ) )
292		iftrue 3878	. . . . . . . . . . . . . . . 16 |- ( j < V -> if ( j < V , j , ( j + 1 ) ) = j )
293	292	eqcomd 2477	. . . . . . . . . . . . . . 15 |- ( j < V -> j = if ( j < V , j , ( j + 1 ) ) )
294	293	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j = if ( j < V , j , ( j + 1 ) ) )
295		zlem1lt 11012	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. ZZ /\ V e. ZZ ) -> ( j <_ V <-> ( j - 1 ) < V ) )
296	239, 199, 295	syl2anr 486	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j <_ V <-> ( j - 1 ) < V ) )
297	259	necomd 2698	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( ( 0 ... N ) \ { V } ) -> V =/= j )
298	297	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> V =/= j )
299		ltlen 9753	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j e. RR /\ V e. RR ) ->