Theorem cvmliftlem10 23825

Description: Lemma for cvmlift 23830. The function K is going to be our complete lifted path, formed by unioning together all the Q functions (each of which is defined on one segment [ ( M - 1 ) / N , M / N ] of the interval). Here we prove by induction that K is a continuous function and a lift of G by applying cvmliftlem6 23821, cvmliftlem7 23822 (to show it is a function and a lift), cvmliftlem8 23823 (to show it is continuous), and cvmliftlem9 23824 (to show that different Q functions agree on the intersection of their domains, so that the pasting lemma paste 17022 gives that K is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)

Hypotheses

Ref	Expression
cvmliftlem.1	|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )
cvmliftlem.b	|- B = U. C
cvmliftlem.x	|- X = U. J
cvmliftlem.f	|- ( ph -> F e. ( C CovMap J ) )
cvmliftlem.g	|- ( ph -> G e. ( II Cn J ) )
cvmliftlem.p	|- ( ph -> P e. B )
cvmliftlem.e	|- ( ph -> ( F ` P ) = ( G ` 0 ) )
cvmliftlem.n	|- ( ph -> N e. NN )
cvmliftlem.t	|- ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
cvmliftlem.a	|- ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
cvmliftlem.l	|- L = ( topGen ` ran (,) )
cvmliftlem.q	|- Q = seq 0 ( ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / N ) [,] ( m / N ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) )
cvmliftlem.k	|- K = U_ k e. ( 1 ... N ) ( Q ` k )
cvmliftlem10.1	|- ( ch <-> ( ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) )

Assertion

Ref	Expression
cvmliftlem10	|- ( ph -> ( K e. ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) )

Distinct variable groups:   v, b, z, B   j, b, k, m, n, s, u, x, F, v, z   n, L, z   P, b, k, m, n, u, v, x, z   C, b, j, k, n, s, u, v, z   ph, j, n, s, x, z   N, b, k, m, n, u, v, x, z   S, b, j, k, n, s, u, v, x, z   j, X   G, b, j, k, m, n, s, u, v, x, z   T, b, j, k, m, s, u, v, x, z   J, b, j, k, n, s, u, v, x, z   Q, b, k, m, n, u, v, x, z

Allowed substitution hints:   ph( v, u, k, m, b)   ch( x, z, v, u, j, k, m, n, s, b)   B( x, u, j, k, m, n, s)   C( x, m)   P( j, s)   Q( j, s)   S( m)   T( n)   J( m)   K( x, z, v, u, j, k, m, n, s, b)   L( x, v, u, j, k, m, s, b)   N( j, s)   X( x, z, v, u, k, m, n, s, b)

Proof of Theorem cvmliftlem10

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvmliftlem.n	. . . 4 |- ( ph -> N e. NN )
2		nnuz 10263	. . . 4 |- NN = ( ZZ>= ` 1 )
3	1, 2	syl6eleq 2373	. . 3 |- ( ph -> N e. ( ZZ>= ` 1 ) )
4		eluzfz2 10804	. . 3 |- ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
5	3, 4	syl 15	. 2 |- ( ph -> N e. ( 1 ... N ) )
6		eleq1 2343	. . . . . 6 |- ( y = 1 -> ( y e. ( 1 ... N ) <-> 1 e. ( 1 ... N ) ) )
7		oveq2 5866	. . . . . . . . . . 11 |- ( y = 1 -> ( 1 ... y ) = ( 1 ... 1 ) )
8		1z 10053	. . . . . . . . . . . 12 |- 1 e. ZZ
9		fzsn 10833	. . . . . . . . . . . 12 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
10	8, 9	ax-mp 8	. . . . . . . . . . 11 |- ( 1 ... 1 ) = { 1 }
11	7, 10	syl6eq 2331	. . . . . . . . . 10 |- ( y = 1 -> ( 1 ... y ) = { 1 } )
12	11	iuneq1d 3928	. . . . . . . . 9 |- ( y = 1 -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. { 1 } ( Q ` k ) )
13		1ex 8833	. . . . . . . . . 10 |- 1 e. _V
14		fveq2 5525	. . . . . . . . . 10 |- ( k = 1 -> ( Q ` k ) = ( Q ` 1 ) )
15	13, 14	iunxsn 3981	. . . . . . . . 9 |- U_ k e. { 1 } ( Q ` k ) = ( Q ` 1 )
16	12, 15	syl6eq 2331	. . . . . . . 8 |- ( y = 1 -> U_ k e. ( 1 ... y ) ( Q ` k ) = ( Q ` 1 ) )
17		oveq1 5865	. . . . . . . . . . 11 |- ( y = 1 -> ( y / N ) = ( 1 / N ) )
18	17	oveq2d 5874	. . . . . . . . . 10 |- ( y = 1 -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( 1 / N ) ) )
19	18	oveq2d 5874	. . . . . . . . 9 |- ( y = 1 -> ( L ↾t ( 0 [,] ( y / N ) ) ) = ( L ↾t ( 0 [,] ( 1 / N ) ) ) )
20	19	oveq1d 5873	. . . . . . . 8 |- ( y = 1 -> ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
21	16, 20	eleq12d 2351	. . . . . . 7 |- ( y = 1 -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) <-> ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) ) )
22	16	coeq2d 4846	. . . . . . . 8 |- ( y = 1 -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. ( Q ` 1 ) ) )
23	18	reseq2d 4955	. . . . . . . 8 |- ( y = 1 -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
24	22, 23	eqeq12d 2297	. . . . . . 7 |- ( y = 1 -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) )
25	21, 24	anbi12d 691	. . . . . 6 |- ( y = 1 -> ( ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) <-> ( ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) )
26	6, 25	imbi12d 311	. . . . 5 |- ( y = 1 -> ( ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) <-> ( 1 e. ( 1 ... N ) -> ( ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) ) )
27	26	imbi2d 307	. . . 4 |- ( y = 1 -> ( ( ph -> ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) ) <-> ( ph -> ( 1 e. ( 1 ... N ) -> ( ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) ) ) )
28		eleq1 2343	. . . . . 6 |- ( y = n -> ( y e. ( 1 ... N ) <-> n e. ( 1 ... N ) ) )
29		oveq2 5866	. . . . . . . . 9 |- ( y = n -> ( 1 ... y ) = ( 1 ... n ) )
30	29	iuneq1d 3928	. . . . . . . 8 |- ( y = n -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
31		oveq1 5865	. . . . . . . . . . 11 |- ( y = n -> ( y / N ) = ( n / N ) )
32	31	oveq2d 5874	. . . . . . . . . 10 |- ( y = n -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( n / N ) ) )
33	32	oveq2d 5874	. . . . . . . . 9 |- ( y = n -> ( L ↾t ( 0 [,] ( y / N ) ) ) = ( L ↾t ( 0 [,] ( n / N ) ) ) )
34	33	oveq1d 5873	. . . . . . . 8 |- ( y = n -> ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) )
35	30, 34	eleq12d 2351	. . . . . . 7 |- ( y = n -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) <-> U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) ) )
36	30	coeq2d 4846	. . . . . . . 8 |- ( y = n -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) )
37	32	reseq2d 4955	. . . . . . . 8 |- ( y = n -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( n / N ) ) ) )
38	36, 37	eqeq12d 2297	. . . . . . 7 |- ( y = n -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) )
39	35, 38	anbi12d 691	. . . . . 6 |- ( y = n -> ( ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) <-> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) )
40	28, 39	imbi12d 311	. . . . 5 |- ( y = n -> ( ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) <-> ( n e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) )
41	40	imbi2d 307	. . . 4 |- ( y = n -> ( ( ph -> ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) ) <-> ( ph -> ( n e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) ) )
42		eleq1 2343	. . . . . 6 |- ( y = ( n + 1 ) -> ( y e. ( 1 ... N ) <-> ( n + 1 ) e. ( 1 ... N ) ) )
43		oveq2 5866	. . . . . . . . 9 |- ( y = ( n + 1 ) -> ( 1 ... y ) = ( 1 ... ( n + 1 ) ) )
44	43	iuneq1d 3928	. . . . . . . 8 |- ( y = ( n + 1 ) -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) )
45		oveq1 5865	. . . . . . . . . . 11 |- ( y = ( n + 1 ) -> ( y / N ) = ( ( n + 1 ) / N ) )
46	45	oveq2d 5874	. . . . . . . . . 10 |- ( y = ( n + 1 ) -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( ( n + 1 ) / N ) ) )
47	46	oveq2d 5874	. . . . . . . . 9 |- ( y = ( n + 1 ) -> ( L ↾t ( 0 [,] ( y / N ) ) ) = ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
48	47	oveq1d 5873	. . . . . . . 8 |- ( y = ( n + 1 ) -> ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
49	44, 48	eleq12d 2351	. . . . . . 7 |- ( y = ( n + 1 ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) <-> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) ) )
50	44	coeq2d 4846	. . . . . . . 8 |- ( y = ( n + 1 ) -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) )
51	46	reseq2d 4955	. . . . . . . 8 |- ( y = ( n + 1 ) -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) )
52	50, 51	eqeq12d 2297	. . . . . . 7 |- ( y = ( n + 1 ) -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
53	49, 52	anbi12d 691	. . . . . 6 |- ( y = ( n + 1 ) -> ( ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) <-> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) ) )
54	42, 53	imbi12d 311	. . . . 5 |- ( y = ( n + 1 ) -> ( ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) <-> ( ( n + 1 ) e. ( 1 ... N ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) ) ) )
55	54	imbi2d 307	. . . 4 |- ( y = ( n + 1 ) -> ( ( ph -> ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( 1 ... N ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) ) ) ) )
56		eleq1 2343	. . . . . 6 |- ( y = N -> ( y e. ( 1 ... N ) <-> N e. ( 1 ... N ) ) )
57		oveq2 5866	. . . . . . . . . 10 |- ( y = N -> ( 1 ... y ) = ( 1 ... N ) )
58	57	iuneq1d 3928	. . . . . . . . 9 |- ( y = N -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... N ) ( Q ` k ) )
59		cvmliftlem.k	. . . . . . . . 9 |- K = U_ k e. ( 1 ... N ) ( Q ` k )
60	58, 59	syl6eqr 2333	. . . . . . . 8 |- ( y = N -> U_ k e. ( 1 ... y ) ( Q ` k ) = K )
61		oveq1 5865	. . . . . . . . . . 11 |- ( y = N -> ( y / N ) = ( N / N ) )
62	61	oveq2d 5874	. . . . . . . . . 10 |- ( y = N -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( N / N ) ) )
63	62	oveq2d 5874	. . . . . . . . 9 |- ( y = N -> ( L ↾t ( 0 [,] ( y / N ) ) ) = ( L ↾t ( 0 [,] ( N / N ) ) ) )
64	63	oveq1d 5873	. . . . . . . 8 |- ( y = N -> ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) )
65	60, 64	eleq12d 2351	. . . . . . 7 |- ( y = N -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) <-> K e. ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) ) )
66	60	coeq2d 4846	. . . . . . . 8 |- ( y = N -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. K ) )
67	62	reseq2d 4955	. . . . . . . 8 |- ( y = N -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( N / N ) ) ) )
68	66, 67	eqeq12d 2297	. . . . . . 7 |- ( y = N -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) )
69	65, 68	anbi12d 691	. . . . . 6 |- ( y = N -> ( ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) <-> ( K e. ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) ) )
70	56, 69	imbi12d 311	. . . . 5 |- ( y = N -> ( ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) <-> ( N e. ( 1 ... N ) -> ( K e. ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) ) ) )
71	70	imbi2d 307	. . . 4 |- ( y = N -> ( ( ph -> ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) ) <-> ( ph -> ( N e. ( 1 ... N ) -> ( K e. ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) ) ) ) )
72		eluzfz1 10803	. . . . . . . . 9 |- ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
73	3, 72	syl 15	. . . . . . . 8 |- ( ph -> 1 e. ( 1 ... N ) )
74		cvmliftlem.1	. . . . . . . . 9 |- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )
75		cvmliftlem.b	. . . . . . . . 9 |- B = U. C
76		cvmliftlem.x	. . . . . . . . 9 |- X = U. J
77		cvmliftlem.f	. . . . . . . . 9 |- ( ph -> F e. ( C CovMap J ) )
78		cvmliftlem.g	. . . . . . . . 9 |- ( ph -> G e. ( II Cn J ) )
79		cvmliftlem.p	. . . . . . . . 9 |- ( ph -> P e. B )
80		cvmliftlem.e	. . . . . . . . 9 |- ( ph -> ( F ` P ) = ( G ` 0 ) )
81		cvmliftlem.t	. . . . . . . . 9 |- ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
82		cvmliftlem.a	. . . . . . . . 9 |- ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
83		cvmliftlem.l	. . . . . . . . 9 |- L = ( topGen ` ran (,) )
84		cvmliftlem.q	. . . . . . . . 9 |- Q = seq 0 ( ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / N ) [,] ( m / N ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) )
85		eqid 2283	. . . . . . . . 9 |- ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) = ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) )
86	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem8 23823	. . . . . . . 8 |- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( Q ` 1 ) e. ( ( L ↾t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) )
87	73, 86	mpdan 649	. . . . . . 7 |- ( ph -> ( Q ` 1 ) e. ( ( L ↾t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) )
88		1m1e0 9814	. . . . . . . . . . . 12 |- ( 1 - 1 ) = 0
89	88	oveq1i 5868	. . . . . . . . . . 11 |- ( ( 1 - 1 ) / N ) = ( 0 / N )
90	1	nncnd 9762	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
91	1	nnne0d 9790	. . . . . . . . . . . 12 |- ( ph -> N =/= 0 )
92	90, 91	div0d 9535	. . . . . . . . . . 11 |- ( ph -> ( 0 / N ) = 0 )
93	89, 92	syl5eq 2327	. . . . . . . . . 10 |- ( ph -> ( ( 1 - 1 ) / N ) = 0 )
94	93	oveq1d 5873	. . . . . . . . 9 |- ( ph -> ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) = ( 0 [,] ( 1 / N ) ) )
95	94	oveq2d 5874	. . . . . . . 8 |- ( ph -> ( L ↾t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) = ( L ↾t ( 0 [,] ( 1 / N ) ) ) )
96	95	oveq1d 5873	. . . . . . 7 |- ( ph -> ( ( L ↾t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
97	87, 96	eleqtrd 2359	. . . . . 6 |- ( ph -> ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
98		simpr 447	. . . . . . . . . 10 |- ( ( ph /\ 1 e. ( 1 ... N ) ) -> 1 e. ( 1 ... N ) )
99	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem7 23822	. . . . . . . . . 10 |- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` ( 1 - 1 ) ) ` ( ( 1 - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( 1 - 1 ) / N ) ) } ) )
100	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99	cvmliftlem6 23821	. . . . . . . . 9 |- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B /\ ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) ) )
101	73, 100	mpdan 649	. . . . . . . 8 |- ( ph -> ( ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B /\ ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) ) )
102	101	simprd 449	. . . . . . 7 |- ( ph -> ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) )
103	94	reseq2d 4955	. . . . . . 7 |- ( ph -> ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
104	102, 103	eqtrd 2315	. . . . . 6 |- ( ph -> ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
105	97, 104	jca 518	. . . . 5 |- ( ph -> ( ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) )
106	105	a1d 22	. . . 4 |- ( ph -> ( 1 e. ( 1 ... N ) -> ( ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) )
107		elnnuz 10264	. . . . . . . . . . 11 |- ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
108	107	biimpi 186	. . . . . . . . . 10 |- ( n e. NN -> n e. ( ZZ>= ` 1 ) )
109	108	adantl 452	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
110		peano2fzr 10808	. . . . . . . . . 10 |- ( ( n e. ( ZZ>= ` 1 ) /\ ( n + 1 ) e. ( 1 ... N ) ) -> n e. ( 1 ... N ) )
111	110	ex 423	. . . . . . . . 9 |- ( n e. ( ZZ>= ` 1 ) -> ( ( n + 1 ) e. ( 1 ... N ) -> n e. ( 1 ... N ) ) )
112	109, 111	syl 15	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( n + 1 ) e. ( 1 ... N ) -> n e. ( 1 ... N ) ) )
113	112	imim1d 69	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( ( n e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) -> ( ( n + 1 ) e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) )
114		cvmliftlem10.1	. . . . . . . . . . 11 |- ( ch <-> ( ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) )
115		eqid 2283	. . . . . . . . . . . . 13 |- U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) = U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) )
116		0re 8838	. . . . . . . . . . . . . . 15 |- 0 e. RR
117	114	simplbi 446	. . . . . . . . . . . . . . . . . . . 20 |- ( ch -> ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) )
118	117	adantl 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) )
119	118	simprd 449	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( n + 1 ) e. ( 1 ... N ) )
120		elfznn 10819	. . . . . . . . . . . . . . . . . 18 |- ( ( n + 1 ) e. ( 1 ... N ) -> ( n + 1 ) e. NN )
121	119, 120	syl 15	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( n + 1 ) e. NN )
122	121	nnred 9761	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( n + 1 ) e. RR )
123	1	adantr 451	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> N e. NN )
124	122, 123	nndivred 9794	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( n + 1 ) / N ) e. RR )
125		iccssre 10731	. . . . . . . . . . . . . . 15 |- ( ( 0 e. RR /\ ( ( n + 1 ) / N ) e. RR ) -> ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR )
126	116, 124, 125	sylancr 644	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR )
127	117	simpld 445	. . . . . . . . . . . . . . . . . . 19 |- ( ch -> n e. NN )
128	127	adantl 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> n e. NN )
129	128	nnred 9761	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> n e. RR )
130	129, 123	nndivred 9794	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( n / N ) e. RR )
131		icccld 18276	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. RR /\ ( n / N ) e. RR ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
132	116, 130, 131	sylancr 644	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
133	83	fveq2i 5528	. . . . . . . . . . . . . . 15 |- ( Clsd ` L ) = ( Clsd ` ( topGen ` ran (,) ) )
134	132, 133	syl6eleqr 2374	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` L ) )
135		ssun1 3338	. . . . . . . . . . . . . . 15 |- ( 0 [,] ( n / N ) ) C_ ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
136	116	a1i 10	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> 0 e. RR )
137	128	nnnn0d 10018	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> n e. NN0 )
138	137	nn0ge0d 10021	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> 0 <_ n )
139	123	nnred 9761	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> N e. RR )
140	123	nngt0d 9789	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> 0 < N )
141		divge0 9625	. . . . . . . . . . . . . . . . . 18 |- ( ( ( n e. RR /\ 0 <_ n ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( n / N ) )
142	129, 138, 139, 140, 141	syl22anc 1183	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> 0 <_ ( n / N ) )
143	129	ltp1d 9687	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> n < ( n + 1 ) )
144		ltdiv1 9620	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. RR /\ ( n + 1 ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( n < ( n + 1 ) <-> ( n / N ) < ( ( n + 1 ) / N ) ) )
145	129, 122, 139, 140, 144	syl112anc 1186	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( n < ( n + 1 ) <-> ( n / N ) < ( ( n + 1 ) / N ) ) )
146	143, 145	mpbid 201	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( n / N ) < ( ( n + 1 ) / N ) )
147	130, 124, 146	ltled 8967	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( n / N ) <_ ( ( n + 1 ) / N ) )
148		elicc2 10715	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. RR /\ ( ( n + 1 ) / N ) e. RR ) -> ( ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) <-> ( ( n / N ) e. RR /\ 0 <_ ( n / N ) /\ ( n / N ) <_ ( ( n + 1 ) / N ) ) ) )
149	116, 124, 148	sylancr 644	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) <-> ( ( n / N ) e. RR /\ 0 <_ ( n / N ) /\ ( n / N ) <_ ( ( n + 1 ) / N ) ) ) )
150	130, 142, 147, 149	mpbir3and 1135	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) )
151		iccsplit 10768	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. RR /\ ( ( n + 1 ) / N ) e. RR /\ ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
152	136, 124, 150, 151	syl3anc 1182	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
153	135, 152	syl5sseqr 3227	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) )
154		uniretop 18271	. . . . . . . . . . . . . . . 16 |- RR = U. ( topGen ` ran (,) )
155	83	unieqi 3837	. . . . . . . . . . . . . . . 16 |- U. L = U. ( topGen ` ran (,) )
156	154, 155	eqtr4i 2306	. . . . . . . . . . . . . . 15 |- RR = U. L
157	156	restcldi 16904	. . . . . . . . . . . . . 14 |- ( ( ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR /\ ( 0 [,] ( n / N ) ) e. ( Clsd ` L ) /\ ( 0 [,] ( n / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
158	126, 134, 153, 157	syl3anc 1182	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
159		icccld 18276	. . . . . . . . . . . . . . . 16 |- ( ( ( n / N ) e. RR /\ ( ( n + 1 ) / N ) e. RR ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
160	130, 124, 159	syl2anc 642	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
161	160, 133	syl6eleqr 2374	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` L ) )
162		ssun2 3339	. . . . . . . . . . . . . . 15 |- ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
163	162, 152	syl5sseqr 3227	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) )
164	156	restcldi 16904	. . . . . . . . . . . . . 14 |- ( ( ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR /\ ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` L ) /\ ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
165	126, 161, 163, 164	syl3anc 1182	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
166		retop 18270	. . . . . . . . . . . . . . . 16 |- ( topGen ` ran (,) ) e. Top
167	83, 166	eqeltri 2353	. . . . . . . . . . . . . . 15 |- L e. Top
168	156	restuni 16893	. . . . . . . . . . . . . . 15 |- ( ( L e. Top /\ ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
169	167, 126, 168	sylancr 644	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
170	152, 169	eqtr3d 2317	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
171	114	simprbi 450	. . . . . . . . . . . . . . . . . . . 20 |- ( ch -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) )
172	171	adantl 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) )
173	172	simpld 445	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) )
174		eqid 2283	. . . . . . . . . . . . . . . . . . 19 |- U. ( L ↾t ( 0 [,] ( n / N ) ) ) = U. ( L ↾t ( 0 [,] ( n / N ) ) )
175	174, 75	cnf 16976	. . . . . . . . . . . . . . . . . 18 |- ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) -> U_ k e. ( 1 ... n ) ( Q ` k ) : U. ( L ↾t ( 0 [,] ( n / N ) ) ) --> B )
176	173, 175	syl 15	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) : U. ( L ↾t ( 0 [,] ( n / N ) ) ) --> B )
177		iccssre 10731	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 0 e. RR /\ ( n / N ) e. RR ) -> ( 0 [,] ( n / N ) ) C_ RR )
178	116, 130, 177	sylancr 644	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) C_ RR )
179	156	restuni 16893	. . . . . . . . . . . . . . . . . . 19 |- ( ( L e. Top /\ ( 0 [,] ( n / N ) ) C_ RR ) -> ( 0 [,] ( n / N ) ) = U. ( L ↾t ( 0 [,] ( n / N ) ) ) )
180	167, 178, 179	sylancr 644	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) = U. ( L ↾t ( 0 [,] ( n / N ) ) ) )
181	180	feq2d 5380	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B <-> U_ k e. ( 1 ... n ) ( Q ` k ) : U. ( L ↾t ( 0 [,] ( n / N ) ) ) --> B ) )
182	176, 181	mpbird 223	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B )
183		eqid 2283	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) = ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) )
184		simpr 447	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( n + 1 ) e. ( 1 ... N ) )
185	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem7 23822	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( ( n + 1 ) - 1 ) / N ) ) } ) )
186	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185	cvmliftlem6 23821	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
187	119, 186	syldan 456	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
188	187	simpld 445	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B )
189	128	nncnd 9762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ch ) -> n e. CC )
190		ax-1cn 8795	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. CC
191		pncan 9057	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
192	189, 190, 191	sylancl 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> ( ( n + 1 ) - 1 ) = n )
193	192	oveq1d 5873	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( ( ( n + 1 ) - 1 ) / N ) = ( n / N ) )
194	193	oveq1d 5873	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) = ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
195	194	feq2d 5380	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B <-> ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B ) )
196	188, 195	mpbid 201	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B )
197		ffun 5391	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B -> Fun U_ k e. ( 1 ... n ) ( Q ` k ) )
198	182, 197	syl 15	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> Fun U_ k e. ( 1 ... n ) ( Q ` k ) )
199	128, 108	syl 15	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> n e. ( ZZ>= ` 1 ) )
200		eluzfz2 10804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. ( ZZ>= ` 1 ) -> n e. ( 1 ... n ) )
201	199, 200	syl 15	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ch ) -> n e. ( 1 ... n ) )
202		fveq2 5525	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = n -> ( Q ` k ) = ( Q ` n ) )
203	202	ssiun2s 3946	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( 1 ... n ) -> ( Q ` n ) C_ U_ k e. ( 1 ... n ) ( Q ` k ) )
204	201, 203	syl 15	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( Q ` n ) C_ U_ k e. ( 1 ... n ) ( Q ` k ) )
205		peano2rem 9113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n e. RR -> ( n - 1 ) e. RR )
206	129, 205	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ch ) -> ( n - 1 ) e. RR )
207	206, 123	nndivred 9794	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) e. RR )
208	207	rexrd 8881	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) e. RR* )
209	130	rexrd 8881	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> ( n / N ) e. RR* )
210	129	ltm1d 9689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ch ) -> ( n - 1 ) < n )
211		ltdiv1 9620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( n - 1 ) e. RR /\ n e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( n - 1 ) < n <-> ( ( n - 1 ) / N ) < ( n / N ) ) )
212	206, 129, 139, 140, 211	syl112anc 1186	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ch ) -> ( ( n - 1 ) < n <-> ( ( n - 1 ) / N ) < ( n / N ) ) )
213	210, 212	mpbid 201	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) < ( n / N ) )
214	207, 130, 213	ltled 8967	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) <_ ( n / N ) )
215		ubicc2 10753	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( n - 1 ) / N ) e. RR* /\ ( n / N ) e. RR* /\ ( ( n - 1 ) / N ) <_ ( n / N ) ) -> ( n / N ) e. ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
216	208, 209, 214, 215	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ch ) -> ( n / N ) e. ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
217	199, 119, 110	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ch ) -> n e. ( 1 ... N ) )
218		eqid 2283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( n - 1 ) / N ) [,] ( n / N ) ) = ( ( ( n - 1 ) / N ) [,] ( n / N ) )
219		simpr 447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ n e. ( 1 ... N ) ) -> n e. ( 1 ... N ) )
220	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218	cvmliftlem7 23822	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( Q ` ( n - 1 ) ) ` ( ( n - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n - 1 ) / N ) ) } ) )
221	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218, 219, 220	cvmliftlem6 23821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B /\ ( F o. ( Q ` n ) ) = ( G |` ( ( ( n - 1 ) / N ) [,] ( n / N ) ) ) ) )
222	217, 221	syldan 456	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ch ) -> ( ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B /\ ( F o. ( Q ` n ) ) = ( G |` ( ( ( n - 1 ) / N ) [,] ( n / N ) ) ) ) )
223	222	simpld 445	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B )
224		fdm 5393	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B -> dom ( Q ` n ) = ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
225	223, 224	syl 15	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ch ) -> dom ( Q ` n ) = ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
226	216, 225	eleqtrrd 2360	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( n / N ) e. dom ( Q ` n ) )
227		funssfv 5543	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( Fun U_ k e. ( 1 ... n ) ( Q ` k ) /\ ( Q ` n ) C_ U_ k e. ( 1 ... n ) ( Q ` k ) /\ ( n / N ) e. dom ( Q ` n ) ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
228	198, 204, 226, 227	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
229	192	fveq2d 5529	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( Q ` ( ( n + 1 ) - 1 ) ) = ( Q ` n ) )
230	229, 193	fveq12d 5531	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ch ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
231	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84	cvmliftlem9 23824	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) )
232	119, 231	syldan 456	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) )
233	193	fveq2d 5529	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
234	232, 233	eqtr3d 2317	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ch ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
235	228, 230, 234	3eqtr2d 2321	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
236	235	opeq2d 3803	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. = <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. )
237	236	sneqd 3653	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> { <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. } = { <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. } )
238		ffn 5389	. . . . . . . . . . . . . . . . . . . 20 |- ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B -> U_ k e. ( 1 ... n ) ( Q ` k ) Fn ( 0 [,] ( n / N ) ) )
239	182, 238	syl 15	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) Fn ( 0 [,] ( n / N ) ) )
240		0xr 8878	. . . . . . . . . . . . . . . . . . . . 21 |- 0 e. RR*
241	240	a1i 10	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> 0 e. RR* )
242		ubicc2 10753	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 0 e. RR* /\ ( n / N ) e. RR* /\ 0 <_ ( n / N ) ) -> ( n / N ) e. ( 0 [,] ( n / N ) ) )
243	241, 209, 142, 242	syl3anc 1182	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( n / N ) e. ( 0 [,] ( n / N ) ) )
244		fnressn 5705	. . . . . . . . . . . . . . . . . . 19 |- ( ( U_ k e. ( 1 ... n ) ( Q ` k ) Fn ( 0 [,] ( n / N ) ) /\ ( n / N ) e. ( 0 [,] ( n / N ) ) ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) = { <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. } )
245	239, 243, 244	syl2anc 642	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) = { <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. } )
246		ffn 5389	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B -> ( Q ` ( n + 1 ) ) Fn ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
247	196, 246	syl 15	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) Fn ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
248	124	rexrd 8881	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> ( ( n + 1 ) / N ) e. RR* )
249		lbicc2 10752	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( n / N ) e. RR* /\ ( ( n + 1 ) / N ) e. RR* /\ ( n / N ) <_ ( ( n + 1 ) / N ) ) -> ( n / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
250	209, 248, 147, 249	syl3anc 1182	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( n / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
251		fnressn 5705	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Q ` ( n + 1 ) ) Fn ( ( n / N ) [,] ( ( n + 1 ) / N ) ) /\ ( n / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) -> ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) = { <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. } )
252	247, 250, 251	syl2anc 642	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) = { <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. } )
253	237, 245, 252	3eqtr4d 2325	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) = ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) )
254		df-icc 10663	. . . . . . . . . . . . . . . . . . . . 21 |- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
255		xrmaxle 10512	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 0 e. RR* /\ ( n / N ) e. RR* /\ z e. RR* ) -> ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) <_ z <-> ( 0 <_ z /\ ( n / N ) <_ z ) ) )
256		xrlemin 10513	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z e. RR* /\ ( n / N ) e. RR* /\ ( ( n + 1 ) / N ) e. RR* ) -> ( z <_ if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) <-> ( z <_ ( n / N ) /\ z <_ ( ( n + 1 ) / N ) ) ) )
257	254, 255, 256	ixxin 10673	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 0 e. RR* /\ ( n / N ) e. RR* ) /\ ( ( n / N ) e. RR* /\ ( ( n + 1 ) / N ) e. RR* ) ) -> ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) [,] if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) ) )
258	241, 209, 209, 248, 257	syl22anc 1183	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) [,] if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) ) )
259		iftrue 3571	. . . . . . . . . . . . . . . . . . . . 21 |- ( 0 <_ ( n / N ) -> if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) = ( n / N ) )
260	142, 259	syl 15	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) = ( n / N ) )
261		iftrue 3571	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n / N ) <_ ( ( n + 1 ) / N ) -> if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) = ( n / N ) )
262	147, 261	syl 15	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) = ( n / N ) )
263	260, 262	oveq12d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) [,] if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) ) = ( ( n / N ) [,] ( n / N ) ) )
264		iccid 10701	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n / N ) e. RR* -> ( ( n / N ) [,] ( n / N ) ) = { ( n / N ) } )
265	209, 264	syl 15	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( n / N ) ) = { ( n / N ) } )
266	258, 263, 265	3eqtrd 2319	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = { ( n / N ) } )
267	266	reseq2d 4955	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) )
268	266	reseq2d 4955	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) )
269	253, 267, 268	3eqtr4d 2325	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
270		fresaun 5412	. . . . . . . . . . . . . . . 16 |- ( ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B /\ ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B )
271	182, 196, 269, 270	syl3anc 1182	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B )
272		fzsuc 10835	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 1 ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
273	199, 272	syl 15	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
274	273	iuneq1d 3928	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) = U_ k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( Q ` k ) )
275		iunxun 3983	. . . . . . . . . . . . . . . . . 18 |- U_ k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( Q ` k ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) u. U_ k e. { ( n + 1 ) } ( Q ` k ) )
276		ovex 5883	. . . . . . . . . . . . . . . . . . . 20 |- ( n + 1 ) e. _V
277		fveq2 5525	. . . . . . . . . . . . . . . . . . . 20 |- ( k = ( n + 1 ) -> ( Q ` k ) = ( Q ` ( n + 1 ) ) )
278	276, 277	iunxsn 3981	. . . . . . . . . . . . . . . . . . 19 |- U_ k e. { ( n + 1 ) } ( Q ` k ) = ( Q ` ( n + 1 ) )
279	278	uneq2i 3326	. . . . . . . . . . . . . . . . . 18 |- ( U_ k e. ( 1 ... n ) ( Q ` k ) u. U_ k e. { ( n + 1 ) } ( Q ` k ) ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) )
280	275, 279	eqtri 2303	. . . . . . . . . . . . . . . . 17 |- U_ k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( Q ` k ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) )
281	274, 280	syl6req 2332	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) = U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) )
282	281	feq1d 5379	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B <-> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B ) )
283	271, 282	mpbid 201	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B )
284	170	feq2d 5380	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B <-> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) --> B ) )
285	283, 284	mpbid 201	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) --> B )
286	281	reseq1d 4954	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( 0 [,] ( n / N ) ) ) = ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( 0 [,] ( n / N ) ) ) )
287		fresaunres1 5414	. . . . . . . . . . . . . . . . 17 |- ( ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B /\ ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( 0 [,] ( n / N ) ) ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
288	182, 196, 269, 287	syl3anc 1182	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( 0 [,] ( n / N ) ) ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
289	286, 288	eqtr3d 2317	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( 0 [,] ( n / N ) ) ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
290	289, 173	eqeltrd 2357	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( 0 [,] ( n / N ) ) ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) )
291	167	a1i 10	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> L e. Top )
292		ovex 5883	. . . . . . . . . . . . . . . . 17 |- ( 0 [,] ( ( n + 1 ) / N ) ) e. _V
293	292	a1i 10	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) e. _V )
294		restabs 16896	. . . . . . . . . . . . . . . 16 |- ( ( L e. Top /\ ( 0 [,] ( n / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) /\ ( 0 [,] ( ( n + 1 ) / N ) ) e. _V ) -> ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( 0 [,] ( n / N ) ) ) = ( L ↾t ( 0 [,] ( n / N ) ) ) )
295	291, 153, 293, 294	syl3anc 1182	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( 0 [,] ( n / N ) ) ) = ( L ↾t ( 0 [,] ( n / N ) ) ) )
296	295	oveq1d 5873	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( 0 [,] ( n / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) )
297	290, 296	eleqtrrd 2360	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( 0 [,] ( n / N ) ) ) e. ( ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( 0 [,] ( n / N ) ) ) Cn C ) )
298	281	reseq1d 4954	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
299		fresaunres2 5413	. . . . . . . . . . . . . . . . 17 |- ( ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B /\ ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( Q ` ( n + 1 ) ) )
300	182, 196, 269, 299	syl3anc 1182	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( Q ` ( n + 1 ) ) )
301	298, 300	eqtr3d 2317	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( Q ` ( n + 1 ) ) )
302	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem8 23823	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( Q ` ( n + 1 ) ) e. ( ( L ↾t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
303	119, 302	syldan 456	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) e. ( ( L ↾t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
304	194	oveq2d 5874	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( L ↾t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) = ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
305	304	oveq1d 5873	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( ( L ↾t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) = ( ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
306	303, 305	eleqtrd 2359	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) e. ( ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
307	301, 306	eqeltrd 2357	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) e. ( ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
308		restabs 16896	. . . . . . . . . . . . . . . 16 |- ( ( L e. Top /\ ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) /\ ( 0 [,] ( ( n + 1 ) / N ) ) e. _V ) -> ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
309	291, 163, 293, 308	syl3anc 1182	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
310	309	oveq1d 5873	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) = ( ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
311	307, 310	eleqtrrd 2360	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) e. ( ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
312	115, 75, 158, 165, 170, 285, 297, 311	paste 17022	. . . . . . . . . . . 12 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
313	152	reseq2d 4955	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) = ( G |` ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
314	172	simprd 449	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) )
315	187	simprd 449	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) )
316	194	reseq2d 4955	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) = ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
317	315, 316	eqtrd 2315	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
318	314, 317	uneq12d 3330	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) u. ( F o. ( Q ` ( n + 1 ) ) ) ) = ( ( G |` ( 0 [,] ( n / N ) ) ) u. ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
319		coundi 5174	. . . . . . . . . . . . . 14 |- ( F o. ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) ) = ( ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) u. ( F o. ( Q ` ( n + 1 ) ) ) )
320		resundi 4969	. . . . . . . . . . . . . 14 |- ( G |` ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( G |` ( 0 [,] ( n / N ) ) ) u. ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
321	318, 319, 320	3eqtr4g 2340	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( F o. ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) ) = ( G |` ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
322	281	coeq2d 4846	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( F o. ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) ) = ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) )
323	313, 321, 322	3eqtr2rd 2322	. . . . . . . . . . . 12 |- ( ( ph /\ ch ) -> ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) )
324	312, 323	jca 518	. . . . . . . . . . 11 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
325	114, 324	sylan2br 462	. . . . . . . . . 10 |- ( ( ph /\ ( ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
326	325	expr 598	. . . . . . . . 9 |- ( ( ph /\ ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) =