Theorem poimirlem24 33433

Description: Lemma for poimir 33442, 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 1843	. . . . . . . . 9 |- F/ j ( ph /\ y e. ( 0 ... ( N - 1 ) ) )
2		nfcsb1v 3549	. . . . . . . . . 10 |- F/_ j [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
3		nfcv 2764	. . . . . . . . . 10 |- F/_ j ( 1 ... N )
4		nfcv 2764	. . . . . . . . . 10 |- F/_ j ( 0 ... K )
5	2, 3, 4	nff 6041	. . . . . . . . 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 1825	. . . . . . . 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 2689	. . . . . . . . . 10 |- ( j = y -> ( j e. ( 0 ... ( N - 1 ) ) <-> y e. ( 0 ... ( N - 1 ) ) ) )
8	7	anbi2d 740	. . . . . . . . 9 |- ( j = y -> ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) <-> ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) ) )
9		csbeq1a 3542	. . . . . . . . . 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 6030	. . . . . . . . 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 334	. . . . . . . 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 11036	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
14		npcan1 10455	. . . . . . . . . . . . 13 |- ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
15	13, 14	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
16	12	nnzd 11481	. . . . . . . . . . . . . 14 |- ( ph -> N e. ZZ )
17		peano2zm 11420	. . . . . . . . . . . . . 14 |- ( N e. ZZ -> ( N - 1 ) e. ZZ )
18	16, 17	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( N - 1 ) e. ZZ )
19		uzid 11702	. . . . . . . . . . . . 13 |- ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
20		peano2uz 11741	. . . . . . . . . . . . 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 2702	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
23		fzss2 12381	. . . . . . . . . . 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 3603	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> j e. ( 0 ... N ) )
26		elun 3753	. . . . . . . . . . . . 13 |- ( y e. ( { 1 } u. { 0 } ) <-> ( y e. { 1 } \/ y e. { 0 } ) )
27		fzofzp1 12565	. . . . . . . . . . . . . . 15 |- ( x e. ( 0..^ K ) -> ( x + 1 ) e. ( 0 ... K ) )
28		elsni 4194	. . . . . . . . . . . . . . . . 17 |- ( y e. { 1 } -> y = 1 )
29	28	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( y e. { 1 } -> ( x + y ) = ( x + 1 ) )
30	29	eleq1d 2686	. . . . . . . . . . . . . . 15 |- ( y e. { 1 } -> ( ( x + y ) e. ( 0 ... K ) <-> ( x + 1 ) e. ( 0 ... K ) ) )
31	27, 30	syl5ibrcom 237	. . . . . . . . . . . . . 14 |- ( x e. ( 0..^ K ) -> ( y e. { 1 } -> ( x + y ) e. ( 0 ... K ) ) )
32		elfzoelz 12470	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( 0..^ K ) -> x e. ZZ )
33	32	zcnd 11483	. . . . . . . . . . . . . . . . 17 |- ( x e. ( 0..^ K ) -> x e. CC )
34	33	addid1d 10236	. . . . . . . . . . . . . . . 16 |- ( x e. ( 0..^ K ) -> ( x + 0 ) = x )
35		elfzofz 12485	. . . . . . . . . . . . . . . 16 |- ( x e. ( 0..^ K ) -> x e. ( 0 ... K ) )
36	34, 35	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( x e. ( 0..^ K ) -> ( x + 0 ) e. ( 0 ... K ) )
37		elsni 4194	. . . . . . . . . . . . . . . . 17 |- ( y e. { 0 } -> y = 0 )
38	37	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( y e. { 0 } -> ( x + y ) = ( x + 0 ) )
39	38	eleq1d 2686	. . . . . . . . . . . . . . 15 |- ( y e. { 0 } -> ( ( x + y ) e. ( 0 ... K ) <-> ( x + 0 ) e. ( 0 ... K ) ) )
40	36, 39	syl5ibrcom 237	. . . . . . . . . . . . . 14 |- ( x e. ( 0..^ K ) -> ( y e. { 0 } -> ( x + y ) e. ( 0 ... K ) ) )
41	31, 40	jaod 395	. . . . . . . . . . . . 13 |- ( x e. ( 0..^ K ) -> ( ( y e. { 1 } \/ y e. { 0 } ) -> ( x + y ) e. ( 0 ... K ) ) )
42	26, 41	syl5bi 232	. . . . . . . . . . . 12 |- ( x e. ( 0..^ K ) -> ( y e. ( { 1 } u. { 0 } ) -> ( x + y ) e. ( 0 ... K ) ) )
43	42	imp 445	. . . . . . . . . . 11 |- ( ( x e. ( 0..^ K ) /\ y e. ( { 1 } u. { 0 } ) ) -> ( x + y ) e. ( 0 ... K ) )
44	43	adantl 482	. . . . . . . . . 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 481	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... N ) ) -> T : ( 1 ... N ) --> ( 0..^ K ) )
47		1ex 10035	. . . . . . . . . . . . . 14 |- 1 e. _V
48	47	fconst 6091	. . . . . . . . . . . . 13 |- ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 }
49		c0ex 10034	. . . . . . . . . . . . . 14 |- 0 e. _V
50	49	fconst 6091	. . . . . . . . . . . . 13 |- ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 }
51	48, 50	pm3.2i 471	. . . . . . . . . . . 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 6143	. . . . . . . . . . . . . . 15 |- ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( U : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' U ) )
54	53	simprbi 480	. . . . . . . . . . . . . 14 |- ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' U )
55		imain 5974	. . . . . . . . . . . . . 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 12433	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( 0 ... N ) -> j e. NN0 )
58	57	nn0red 11352	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... N ) -> j e. RR )
59	58	ltp1d 10954	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... N ) -> j < ( j + 1 ) )
60		fzdisj 12368	. . . . . . . . . . . . . . . 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 5466	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... N ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( U " (/) ) )
63		ima0 5481	. . . . . . . . . . . . . 14 |- ( U " (/) ) = (/)
64	62, 63	syl6eq 2672	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... N ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = (/) )
65	56, 64	sylan9req 2677	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) )
66		fun 6066	. . . . . . . . . . . 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 695	. . . . . . . . . . 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 11332	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN0 -> ( j + 1 ) e. NN )
69	57, 68	syl 17	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... N ) -> ( j + 1 ) e. NN )
70		nnuz 11723	. . . . . . . . . . . . . . . . 17 |- NN = ( ZZ>= ` 1 )
71	69, 70	syl6eleq 2711	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... N ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
72		elfzuz3 12339	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... N ) -> N e. ( ZZ>= ` j ) )
73		fzsplit2 12366	. . . . . . . . . . . . . . . 16 |- ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` j ) ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
74	71, 72, 73	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... N ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
75	74	imaeq2d 5466	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... N ) -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) )
76		imaundi 5545	. . . . . . . . . . . . . 14 |- ( U " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) )
77	75, 76	syl6req 2673	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... N ) -> ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) = ( U " ( 1 ... N ) ) )
78		f1ofo 6144	. . . . . . . . . . . . . 14 |- ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) -onto-> ( 1 ... N ) )
79		foima 6120	. . . . . . . . . . . . . 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 2678	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
82	81	feq2d 6031	. . . . . . . . . . 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 222	. . . . . . . . . 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 6678	. . . . . . . . . . 11 |- ( 1 ... N ) e. _V
85	84	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( 1 ... N ) e. _V )
86		inidm 3822	. . . . . . . . . 10 |- ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
87	44, 46, 83, 85, 85, 86	off 6912	. . . . . . . . 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 487	. . . . . . . 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 2262	. . . . . . 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 12394	. . . . . . . . 9 |- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) )
91	15	oveq2d 6666	. . . . . . . . . . 11 |- ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
92	91	eleq2d 2687	. . . . . . . . . 10 |- ( ph -> ( ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) <-> ( y + 1 ) e. ( 0 ... N ) ) )
93	92	biimpa 501	. . . . . . . . 9 |- ( ( ph /\ ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) ) -> ( y + 1 ) e. ( 0 ... N ) )
94	90, 93	sylan2 491	. . . . . . . 8 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y + 1 ) e. ( 0 ... N ) )
95		nfv 1843	. . . . . . . . . 10 |- F/ j ( ph /\ ( y + 1 ) e. ( 0 ... N ) )
96		nfcsb1v 3549	. . . . . . . . . . 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 6041	. . . . . . . . . 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 1825	. . . . . . . . 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 6678	. . . . . . . . 9 |- ( y + 1 ) e. _V
100		eleq1 2689	. . . . . . . . . . 11 |- ( j = ( y + 1 ) -> ( j e. ( 0 ... N ) <-> ( y + 1 ) e. ( 0 ... N ) ) )
101	100	anbi2d 740	. . . . . . . . . 10 |- ( j = ( y + 1 ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) ) )
102		csbeq1a 3542	. . . . . . . . . . 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 6030	. . . . . . . . . 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 334	. . . . . . . . 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 3258	. . . . . . . 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 487	. . . . . . 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 3536	. . . . . . . . 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 6030	. . . . . . . 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 3536	. . . . . . . . 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 6030	. . . . . . . 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 4124	. . . . . . 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 693	. . . . . 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 6678	. . . . . . 7 |- ( 0 ... K ) e. _V
114	113, 84	elmap 7886	. . . . . 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 224	. . . . 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 2622	. . . . 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 6385	. . . 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 6678	. . . . 5 |- ( ( 0 ... K ) ^m ( 1 ... N ) ) e. _V
119		ovex 6678	. . . . 5 |- ( 0 ... ( N - 1 ) ) e. _V
120	118, 119	elmap 7886	. . . 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 224	. . 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 5351	. . . . . . . 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 4738	. . . . . . 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 5353	. . . . . 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 3633	. . . . 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 3145	. . . . 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 747	. . . 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 3336	. . 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 3592	. . . 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 6678	. . . . . . . . . . . . 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 3559	. . . . . . . . . . . 12 |- [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = C
134	133	csbeq2i 3993	. . . . . . . . . . 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 4932	. . . . . . . . . . . . 13 |- <. T , U >. e. _V
136	135	a1i 11	. . . . . . . . . . . 12 |- ( ph -> <. T , U >. e. _V )
137		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( s = <. T , U >. -> ( 1st ` s ) = ( 1st ` <. T , U >. ) )
138		fex 6490	. . . . . . . . . . . . . . . . 17 |- ( ( T : ( 1 ... N ) --> ( 0..^ K ) /\ ( 1 ... N ) e. _V ) -> T e. _V )
139	45, 84, 138	sylancl 694	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. _V )
140		f1oexrnex 7115	. . . . . . . . . . . . . . . . 17 |- ( ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( 1 ... N ) e. _V ) -> U e. _V )
141	52, 84, 140	sylancl 694	. . . . . . . . . . . . . . . 16 |- ( ph -> U e. _V )
142		op1stg 7180	. . . . . . . . . . . . . . . 16 |- ( ( T e. _V /\ U e. _V ) -> ( 1st ` <. T , U >. ) = T )
143	139, 141, 142	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1st ` <. T , U >. ) = T )
144	137, 143	sylan9eqr 2678	. . . . . . . . . . . . . 14 |- ( ( ph /\ s = <. T , U >. ) -> ( 1st ` s ) = T )
145		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( s = <. T , U >. -> ( 2nd ` s ) = ( 2nd ` <. T , U >. ) )
146		op2ndg 7181	. . . . . . . . . . . . . . . . 17 |- ( ( T e. _V /\ U e. _V ) -> ( 2nd ` <. T , U >. ) = U )
147	139, 141, 146	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2nd ` <. T , U >. ) = U )
148	145, 147	sylan9eqr 2678	. . . . . . . . . . . . . . 15 |- ( ( ph /\ s = <. T , U >. ) -> ( 2nd ` s ) = U )
149		imaeq1 5461	. . . . . . . . . . . . . . . . 17 |- ( ( 2nd ` s ) = U -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( U " ( 1 ... j ) ) )
150	149	xpeq1d 5138	. . . . . . . . . . . . . . . 16 |- ( ( 2nd ` s ) = U -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... j ) ) X. { 1 } ) )
151		imaeq1 5461	. . . . . . . . . . . . . . . . 17 |- ( ( 2nd ` s ) = U -> ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) = ( U " ( ( j + 1 ) ... N ) ) )
152	151	xpeq1d 5138	. . . . . . . . . . . . . . . 16 |- ( ( 2nd ` s ) = U -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
153	150, 152	uneq12d 3768	. . . . . . . . . . . . . . 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 6668	. . . . . . . . . . . . 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 3540	. . . . . . . . . . . 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 3560	. . . . . . . . . . 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 2670	. . . . . . . . . 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 3992	. . . . . . . . 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 2632	. . . . . . . 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 3052	. . . . . . 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 3203	. . . . . . . . 9 |- i e. _V
163		eqid 2622	. . . . . . . . . 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 5372	. . . . . . . . 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 1843	. . . . . . . . 9 |- F/ k i = B
167		nfcsb1v 3549	. . . . . . . . . 10 |- F/_ p [_ k / p ]_ B
168	167	nfeq2 2780	. . . . . . . . 9 |- F/ p i = [_ k / p ]_ B
169		csbeq1a 3542	. . . . . . . . . 10 |- ( p = k -> B = [_ k / p ]_ B )
170	169	eqeq2d 2632	. . . . . . . . 9 |- ( p = k -> ( i = B <-> i = [_ k / p ]_ B ) )
171	166, 168, 170	cbvrex 3168	. . . . . . . 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 6678	. . . . . . . . . . 11 |- ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
173	172	csbex 4793	. . . . . . . . . 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 2924	. . . . . . . . 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 3536	. . . . . . . . . . . 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 3203	. . . . . . . . . . . . . 14 |- y e. _V
177	176, 99	ifex 4156	. . . . . . . . . . . . 13 |- if ( y < V , y , ( y + 1 ) ) e. _V
178		csbnestg 3998	. . . . . . . . . . . . 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 2674	. . . . . . . . . . 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 2632	. . . . . . . . . 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 6369	. . . . . . . . 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 286	. . . . . . 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 278	. . . . . 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 3603	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. ( 0 ... N ) )
187	186	adantr 481	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y e. ( 0 ... N ) )
188		elfzelz 12342	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ... ( N - 1 ) ) -> y e. ZZ )
189	188	zred 11482	. . . . . . . . . . . . 13 |- ( y e. ( 0 ... ( N - 1 ) ) -> y e. RR )
190	189	adantl 482	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. RR )
191		ltne 10134	. . . . . . . . . . . . 13 |- ( ( y e. RR /\ y < V ) -> V =/= y )
192	191	necomd 2849	. . . . . . . . . . . 12 |- ( ( y e. RR /\ y < V ) -> y =/= V )
193	190, 192	sylan 488	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y =/= V )
194		eldifsn 4317	. . . . . . . . . . 11 |- ( y e. ( ( 0 ... N ) \ { V } ) <-> ( y e. ( 0 ... N ) /\ y =/= V ) )
195	187, 193, 194	sylanbrc 698	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y e. ( ( 0 ... N ) \ { V } ) )
196	94	adantr 481	. . . . . . . . . . 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 12342	. . . . . . . . . . . . . . 15 |- ( V e. ( 0 ... N ) -> V e. ZZ )
199	197, 198	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> V e. ZZ )
200	199	zred 11482	. . . . . . . . . . . . 13 |- ( ph -> V e. RR )
201	200	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> V e. RR )
202		zre 11381	. . . . . . . . . . . . . . . 16 |- ( V e. ZZ -> V e. RR )
203		zre 11381	. . . . . . . . . . . . . . . 16 |- ( y e. ZZ -> y e. RR )
204		lenlt 10116	. . . . . . . . . . . . . . . 16 |- ( ( V e. RR /\ y e. RR ) -> ( V <_ y <-> -. y < V ) )
205	202, 203, 204	syl2an 494	. . . . . . . . . . . . . . 15 |- ( ( V e. ZZ /\ y e. ZZ ) -> ( V <_ y <-> -. y < V ) )
206		zleltp1 11428	. . . . . . . . . . . . . . 15 |- ( ( V e. ZZ /\ y e. ZZ ) -> ( V <_ y <-> V < ( y + 1 ) ) )
207	205, 206	bitr3d 270	. . . . . . . . . . . . . 14 |- ( ( V e. ZZ /\ y e. ZZ ) -> ( -. y < V <-> V < ( y + 1 ) ) )
208	199, 188, 207	syl2an 494	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( -. y < V <-> V < ( y + 1 ) ) )
209	208	biimpa 501	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> V < ( y + 1 ) )
210	201, 209	gtned 10172	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) =/= V )
211		eldifsn 4317	. . . . . . . . . . 11 |- ( ( y + 1 ) e. ( ( 0 ... N ) \ { V } ) <-> ( ( y + 1 ) e. ( 0 ... N ) /\ ( y + 1 ) =/= V ) )
212	196, 210, 211	sylanbrc 698	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) e. ( ( 0 ... N ) \ { V } ) )
213	195, 212	ifclda 4120	. . . . . . . . 9 |- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < V , y , ( y + 1 ) ) e. ( ( 0 ... N ) \ { V } ) )
214		nfcsb1v 3549	. . . . . . . . . . . 12 |- F/_ j [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
215	214	nfeq2 2780	. . . . . . . . . . 11 |- F/ j i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
216		csbeq1a 3542	. . . . . . . . . . . 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 2632	. . . . . . . . . . 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 3304	. . . . . . . . . 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 450	. . . . . . . . 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 3031	. . . . . . 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 1843	. . . . . . . 8 |- F/ j ph
223		nfcv 2764	. . . . . . . . 9 |- F/_ j ( 0 ... ( N - 1 ) )
224	223, 215	nfrex 3007	. . . . . . . 8 |- F/ j E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
225		eldifi 3732	. . . . . . . . . . . . . . 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 11354	. . . . . . . . . . . . 13 |- ( j e. ( ( 0 ... N ) \ { V } ) -> 0 <_ j )
228	227	ad2antlr 763	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> 0 <_ j )
229	226	nn0red 11352	. . . . . . . . . . . . . . 15 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j e. RR )
230	229	ad2antlr 763	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j e. RR )
231	200	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> V e. RR )
232	16	zred 11482	. . . . . . . . . . . . . . 15 |- ( ph -> N e. RR )
233	232	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> N e. RR )
234		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j < V )
235		elfzle2 12345	. . . . . . . . . . . . . . . 16 |- ( V e. ( 0 ... N ) -> V <_ N )
236	197, 235	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> V <_ N )
237	236	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> V <_ N )
238	230, 231, 233, 234, 237	ltletrd 10197	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j < N )
239	226	nn0zd 11480	. . . . . . . . . . . . . . 15 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j e. ZZ )
240		zltlem1 11430	. . . . . . . . . . . . . . 15 |- ( ( j e. ZZ /\ N e. ZZ ) -> ( j < N <-> j <_ ( N - 1 ) ) )
241	239, 16, 240	syl2anr 495	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j < N <-> j <_ ( N - 1 ) ) )
242	241	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> ( j < N <-> j <_ ( N - 1 ) ) )
243	238, 242	mpbid 222	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j <_ ( N - 1 ) )
244		0z 11388	. . . . . . . . . . . . . . 15 |- 0 e. ZZ
245		elfz 12332	. . . . . . . . . . . . . . 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 1412	. . . . . . . . . . . . . 14 |- ( ( j e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
247	239, 18, 246	syl2anr 495	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
248	247	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
249	228, 243, 248	mpbir2and 957	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j e. ( 0 ... ( N - 1 ) ) )
250		0red 10041	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 e. RR )
251	200	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V e. RR )
252	229	ad2antlr 763	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j e. RR )
253		elfzle1 12344	. . . . . . . . . . . . . . . . 17 |- ( V e. ( 0 ... N ) -> 0 <_ V )
254	197, 253	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ V )
255	254	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 <_ V )
256		lenlt 10116	. . . . . . . . . . . . . . . . . 18 |- ( ( V e. RR /\ j e. RR ) -> ( V <_ j <-> -. j < V ) )
257	200, 229, 256	syl2an 494	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( V <_ j <-> -. j < V ) )
258	257	biimpar 502	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V <_ j )
259		eldifsni 4320	. . . . . . . . . . . . . . . . 17 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j =/= V )
260	259	ad2antlr 763	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j =/= V )
261		ltlen 10138	. . . . . . . . . . . . . . . . . 18 |- ( ( V e. RR /\ j e. RR ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
262	200, 229, 261	syl2an 494	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
263	262	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
264	258, 260, 263	mpbir2and 957	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V < j )
265	250, 251, 252, 255, 264	lelttrd 10195	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 < j )
266		zgt0ge1 11431	. . . . . . . . . . . . . . . 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 763	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( 0 < j <-> 1 <_ j ) )
269	265, 268	mpbid 222	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 1 <_ j )
270		elfzle2 12345	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... N ) -> j <_ N )
271	225, 270	syl 17	. . . . . . . . . . . . . 14 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j <_ N )
272	271	ad2antlr 763	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j <_ N )
273		1z 11407	. . . . . . . . . . . . . . . 16 |- 1 e. ZZ
274		elfz 12332	. . . . . . . . . . . . . . . 16 |- ( ( j e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
275	273, 274	mp3an2 1412	. . . . . . . . . . . . . . 15 |- ( ( j e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
276	239, 16, 275	syl2anr 495	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
277	276	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
278	269, 272, 277	mpbir2and 957	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j e. ( 1 ... N ) )
279		elfzmlbm 12449	. . . . . . . . . . . 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 4120	. . . . . . . . . 10 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> if ( j < V , j , ( j - 1 ) ) e. ( 0 ... ( N - 1 ) ) )
282		breq1 4656	. . . . . . . . . . . . . . . 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 6657	. . . . . . . . . . . . . . . 16 |- ( j = if ( j < V , j , ( j - 1 ) ) -> ( j + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
285	282, 283, 284	ifbieq12d 4113	. . . . . . . . . . . . . . 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 2632	. . . . . . . . . . . . . 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 4656	. . . . . . . . . . . . . . . 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 6657	. . . . . . . . . . . . . . . 16 |- ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( ( j - 1 ) + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
290	287, 288, 289	ifbieq12d 4113	. . . . . . . . . . . . . . 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 2632	. . . . . . . . . . . . . 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 4092	. . . . . . . . . . . . . . . 16 |- ( j < V -> if ( j < V , j , ( j + 1 ) ) = j )
293	292	eqcomd 2628	. . . . . . . . . . . . . . 15 |- ( j < V -> j = if ( j < V , j , ( j + 1 ) ) )
294	293	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j = if ( j < V , j , ( j + 1 ) ) )
295		zlem1lt 11429	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. ZZ /\ V e. ZZ ) -> ( j <_ V <-> ( j - 1 ) < V ) )
296	239, 199, 295	syl2anr 495	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j <_ V <-> ( j - 1 ) < V ) )
297	259	necomd 2849	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( ( 0 ... N ) \ { V } ) -> V =/= j )
298	297	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> V =/= j )
299		ltlen 10138	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j e. RR /\ V e. RR ) -> ( j < V <-> ( j <_ V /\ V =/= j ) ) )
300	229, 200, 299	syl2anr 495	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j < V <-> ( j <_ V /\ V =/= j ) ) )
301	300	biimprd 238	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( ( j <_ V /\ V =/= j ) -> j < V ) )
302	298, 301	mpan2d 710	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j <_ V -> j < V ) )
303	296, 302	sylbird 250	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( ( j - 1 ) < V -> j < V ) )
304	303	con3dimp 457	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> -. ( j - 1 ) < V )
305	304	iffalsed 4097	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) = ( ( j - 1 ) + 1 ) )
306	226	nn0cnd 11353	. . . . . . . . . . . . . . . . 17 |- ( j e. ( ( 0 ... N ) \ { V } ) -> j e. CC )
307		npcan1 10455	. . . . . . . . . . . . . . . . 17 |- ( j e. CC -> ( ( j - 1 ) + 1 ) = j )
308	306, 307	syl 17	. . . . . . . . . . . . . . . 16 |- ( j e. ( ( 0 ... N ) \ { V } ) -> ( ( j - 1 ) + 1 ) = j )
309	308	ad2antlr 763	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( ( j - 1 ) + 1 ) = j )
310	305, 309	eqtr2d 2657	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j = if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) )
311	286, 291, 294, 310	ifbothda 4123	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> j = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) )
312		csbeq1a 3542	. . . . . . . . . . . . 13 |- ( j = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) -> [_ <. T , U >. / s ]_ C = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
313	311, 312	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> [_ <. T , U >. / s ]_ C = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
314	313	eqeq2d 2632	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( i = [_ <. T , U >. / s ]_ C <-> i = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
315	314	biimpd 219	. . . . . . . . . 10 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( i = [_ <. T , U >. / s ]_ C -> i = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
316		breq1 4656	. . . . . . . . . . . . . 14 |- ( y = if ( j < V , j , ( j - 1 ) ) -> ( y < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
317		id 22	. . . . . . . . . . . . . 14 |- ( y = if ( j < V , j , ( j - 1 ) ) -> y = if ( j < V , j , ( j - 1 ) ) )
318		oveq1 6657	. . . . . . . . . . . . . 14 |- ( y = if ( j < V , j , ( j - 1 ) ) -> ( y + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
319	316, 317, 318	ifbieq12d 4113	. . . . . . . . . . . . 13 |- ( y = if ( j < V , j , ( j - 1 ) ) -> if ( y < V , y , ( y + 1 ) ) = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) )
320	319	csbeq1d 3540	. . . . . . . . . . . 12 |- ( y = if ( j < V , j , ( j - 1 ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
321	320	eqeq2d 2632	. . . . . . . . . . 11 |- ( y = if ( j < V , j , ( j - 1 ) ) -> ( i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> i = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
322	321	rspcev 3309	. . . . . . . . . 10 |- ( ( if ( j < V , j , ( j - 1 ) ) e. ( 0 ... ( N - 1 ) ) /\ i = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) -> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
323	281, 315, 322	syl6an 568	. . . . . . . . 9 |- ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( i = [_ <. T , U >. / s ]_ C -> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
324	323	ex 450	. . . . . . . 8 |- ( ph -> ( j e. ( ( 0 ... N ) \ { V } ) -> ( i = [_ <. T , U >. / s ]_ C -> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) ) )
325	222, 224, 324	rexlimd 3026	. . . . . . 7 |- ( ph -> ( E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C -> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
326	221, 325	impbid 202	. . . . . 6 |- ( 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 ) )
327	185, 326	bitr3d 270	. . . . 5 |- ( ph -> ( 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. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
328	327	ralbidv 2986	. . . 4 |- ( ph -> ( 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 ) <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
329	130, 328	syl5bb 272	. . 3 |- ( ph -> ( ( 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 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
330	329	anbi1d 741	. 2 |- ( ph -> ( ( ( 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 ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C /\ 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 ) ) )
331	12, 45, 52, 197	poimirlem23 33432	. . 3 |- ( ph -> ( 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 <-> -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) )
332	331	anbi2d 740	. 2 |- ( ph -> ( ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C /\ 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 ) <-> ( 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 ) ) ) ) )
333	129, 330, 332	3bitrd 294	1 |- ( 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 ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   [_csb 3533   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   ran crn 5115   "cima 5117   Fun wfun 5882   -->wf 5884   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   oFcof 6895   1stc1st 7166   2ndc2nd 7167   ^m cmap 7857   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   < clt 10074   <_ cle 10075   - cmin 10266   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326  ..^cfzo 12465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466

This theorem is referenced by:  poimirlem27  33436