Theorem cvmliftlem8 27315

Description: Lemma for cvmlift 27322. The functions Q are continuous functions because they are defined as `' ( F |` I ) o. G where G is continuous and ( F |` I ) is a homeomorphism. (Contributed by Mario Carneiro, 16-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 >. } >. } ) )
cvmliftlem5.3	|- W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )

Assertion

Ref	Expression
cvmliftlem8	|- ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) e. ( ( L ↾t W ) Cn C ) )

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

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

Proof of Theorem cvmliftlem8

Step	Hyp	Ref	Expression
1		elfznn 11579	. . 3 |- ( M e. ( 1 ... N ) -> M e. NN )
2		cvmliftlem.1	. . . 4 |- 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 ) ) ) ) } )
3		cvmliftlem.b	. . . 4 |- B = U. C
4		cvmliftlem.x	. . . 4 |- X = U. J
5		cvmliftlem.f	. . . 4 |- ( ph -> F e. ( C CovMap J ) )
6		cvmliftlem.g	. . . 4 |- ( ph -> G e. ( II Cn J ) )
7		cvmliftlem.p	. . . 4 |- ( ph -> P e. B )
8		cvmliftlem.e	. . . 4 |- ( ph -> ( F ` P ) = ( G ` 0 ) )
9		cvmliftlem.n	. . . 4 |- ( ph -> N e. NN )
10		cvmliftlem.t	. . . 4 |- ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
11		cvmliftlem.a	. . . 4 |- ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
12		cvmliftlem.l	. . . 4 |- L = ( topGen ` ran (,) )
13		cvmliftlem.q	. . . 4 |- 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 >. } >. } ) )
14		cvmliftlem5.3	. . . 4 |- W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
15	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14	cvmliftlem5 27312	. . 3 |- ( ( ph /\ M e. NN ) -> ( Q ` M ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
16	1, 15	sylan2 474	. 2 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
17	5	adantr 465	. . . 4 |- ( ( ph /\ M e. ( 1 ... N ) ) -> F e. ( C CovMap J ) )
18		cvmtop1 27283	. . . 4 |- ( F e. ( C CovMap J ) -> C e. Top )
19		cnrest2r 19007	. . . 4 |- ( C e. Top -> ( ( L ↾t W ) Cn ( C ↾t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) C_ ( ( L ↾t W ) Cn C ) )
20	17, 18, 19	3syl 20	. . 3 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( L ↾t W ) Cn ( C ↾t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) C_ ( ( L ↾t W ) Cn C ) )
21		retopon 20458	. . . . . 6 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
22	12, 21	eqeltri 2535	. . . . 5 |- L e. (TopOn ` RR )
23		simpr 461	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. ( 1 ... N ) )
24	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14	cvmliftlem2 27309	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ ( 0 [,] 1 ) )
25		unitssre 11533	. . . . . 6 |- ( 0 [,] 1 ) C_ RR
26	24, 25	syl6ss 3466	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ RR )
27		resttopon 18881	. . . . 5 |- ( ( L e. (TopOn ` RR ) /\ W C_ RR ) -> ( L ↾t W ) e. (TopOn ` W ) )
28	22, 26, 27	sylancr 663	. . . 4 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( L ↾t W ) e. (TopOn ` W ) )
29		eqid 2451	. . . . . . 7 |- ( II ↾t W ) = ( II ↾t W )
30		iitopon 20571	. . . . . . . 8 |- II e. (TopOn ` ( 0 [,] 1 ) )
31	30	a1i 11	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> II e. (TopOn ` ( 0 [,] 1 ) ) )
32	6	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G e. ( II Cn J ) )
33		iiuni 20573	. . . . . . . . . . 11 |- ( 0 [,] 1 ) = U. II
34	33, 4	cnf 18966	. . . . . . . . . 10 |- ( G e. ( II Cn J ) -> G : ( 0 [,] 1 ) --> X )
35	32, 34	syl 16	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G : ( 0 [,] 1 ) --> X )
36	35	feqmptd 5843	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G = ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) )
37	36, 32	eqeltrrd 2540	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) e. ( II Cn J ) )
38	29, 31, 24, 37	cnmpt1res 19365	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( II ↾t W ) Cn J ) )
39		dfii2 20574	. . . . . . . . . 10 |- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
40	12	oveq1i 6200	. . . . . . . . . 10 |- ( L ↾t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
41	39, 40	eqtr4i 2483	. . . . . . . . 9 |- II = ( L ↾t ( 0 [,] 1 ) )
42	41	oveq1i 6200	. . . . . . . 8 |- ( II ↾t W ) = ( ( L ↾t ( 0 [,] 1 ) ) ↾t W )
43		retop 20456	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) e. Top
44	12, 43	eqeltri 2535	. . . . . . . . . 10 |- L e. Top
45	44	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> L e. Top )
46		ovex 6215	. . . . . . . . . 10 |- ( 0 [,] 1 ) e. _V
47	46	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 0 [,] 1 ) e. _V )
48		restabs 18885	. . . . . . . . 9 |- ( ( L e. Top /\ W C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) e. _V ) -> ( ( L ↾t ( 0 [,] 1 ) ) ↾t W ) = ( L ↾t W ) )
49	45, 24, 47, 48	syl3anc 1219	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( L ↾t ( 0 [,] 1 ) ) ↾t W ) = ( L ↾t W ) )
50	42, 49	syl5eq 2504	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( II ↾t W ) = ( L ↾t W ) )
51	50	oveq1d 6205	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( II ↾t W ) Cn J ) = ( ( L ↾t W ) Cn J ) )
52	38, 51	eleqtrd 2541	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn J ) )
53		cvmtop2 27284	. . . . . . . 8 |- ( F e. ( C CovMap J ) -> J e. Top )
54	17, 53	syl 16	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> J e. Top )
55	4	toptopon 18654	. . . . . . 7 |- ( J e. Top <-> J e. (TopOn ` X ) )
56	54, 55	sylib 196	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> J e. (TopOn ` X ) )
57		simprl 755	. . . . . . . . . 10 |- ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> M e. ( 1 ... N ) )
58		simprr 756	. . . . . . . . . 10 |- ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> z e. W )
59	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 57, 14, 58	cvmliftlem3 27310	. . . . . . . . 9 |- ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
60	59	anassrs 648	. . . . . . . 8 |- ( ( ( ph /\ M e. ( 1 ... N ) ) /\ z e. W ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
61		eqid 2451	. . . . . . . 8 |- ( z e. W |-> ( G ` z ) ) = ( z e. W |-> ( G ` z ) )
62	60, 61	fmptd 5966	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) : W --> ( 1st ` ( T ` M ) ) )
63		frn 5663	. . . . . . 7 |- ( ( z e. W |-> ( G ` z ) ) : W --> ( 1st ` ( T ` M ) ) -> ran ( z e. W |-> ( G ` z ) ) C_ ( 1st ` ( T ` M ) ) )
64	62, 63	syl 16	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ran ( z e. W |-> ( G ` z ) ) C_ ( 1st ` ( T ` M ) ) )
65	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23	cvmliftlem1 27308	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
66	2	cvmsrcl 27287	. . . . . . . 8 |- ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) -> ( 1st ` ( T ` M ) ) e. J )
67		elssuni 4219	. . . . . . . 8 |- ( ( 1st ` ( T ` M ) ) e. J -> ( 1st ` ( T ` M ) ) C_ U. J )
68	65, 66, 67	3syl 20	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ U. J )
69	68, 4	syl6sseqr 3501	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ X )
70		cnrest2 19006	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ ran ( z e. W |-> ( G ` z ) ) C_ ( 1st ` ( T ` M ) ) /\ ( 1st ` ( T ` M ) ) C_ X ) -> ( ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn J ) <-> ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn ( J ↾t ( 1st ` ( T ` M ) ) ) ) ) )
71	56, 64, 69, 70	syl3anc 1219	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn J ) <-> ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn ( J ↾t ( 1st ` ( T ` M ) ) ) ) ) )
72	52, 71	mpbid 210	. . . 4 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn ( J ↾t ( 1st ` ( T ` M ) ) ) ) )
73	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14	cvmliftlem7 27314	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
74		cvmcn 27285	. . . . . . . . . . . 12 |- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
75	3, 4	cnf 18966	. . . . . . . . . . . 12 |- ( F e. ( C Cn J ) -> F : B --> X )
76	17, 74, 75	3syl 20	. . . . . . . . . . 11 |- ( ( ph /\ M e. ( 1 ... N ) ) -> F : B --> X )
77		ffn 5657	. . . . . . . . . . 11 |- ( F : B --> X -> F Fn B )
78		fniniseg 5923	. . . . . . . . . . 11 |- ( F Fn B -> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) <-> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) ) ) )
79	76, 77, 78	3syl 20	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) <-> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) ) ) )
80	73, 79	mpbid 210	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) ) )
81	80	simpld 459	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B )
82	80	simprd 463	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) )
83	1	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. NN )
84	83	nnred 10438	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. RR )
85		peano2rem 9776	. . . . . . . . . . . . . . 15 |- ( M e. RR -> ( M - 1 ) e. RR )
86	84, 85	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) e. RR )
87	9	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> N e. NN )
88	86, 87	nndivred 10471	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR )
89	88	rexrd 9534	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR* )
90	84, 87	nndivred 10471	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR )
91	90	rexrd 9534	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR* )
92	84	ltm1d 10366	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) < M )
93	87	nnred 10438	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> N e. RR )
94	87	nngt0d 10466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> 0 < N )
95		ltdiv1 10294	. . . . . . . . . . . . . . 15 |- ( ( ( M - 1 ) e. RR /\ M e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( M - 1 ) < M <-> ( ( M - 1 ) / N ) < ( M / N ) ) )
96	86, 84, 93, 94, 95	syl112anc 1223	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) < M <-> ( ( M - 1 ) / N ) < ( M / N ) ) )
97	92, 96	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) < ( M / N ) )
98	88, 90, 97	ltled 9623	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) <_ ( M / N ) )
99		lbicc2 11502	. . . . . . . . . . . 12 |- ( ( ( ( M - 1 ) / N ) e. RR* /\ ( M / N ) e. RR* /\ ( ( M - 1 ) / N ) <_ ( M / N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
100	89, 91, 98, 99	syl3anc 1219	. . . . . . . . . . 11 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
101	100, 14	syl6eleqr 2550	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. W )
102	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14, 101	cvmliftlem3 27310	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( G ` ( ( M - 1 ) / N ) ) e. ( 1st ` ( T ` M ) ) )
103	82, 102	eqeltrd 2539	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) )
104		eqid 2451	. . . . . . . . 9 |- ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) = ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b )
105	2, 3, 104	cvmsiota 27300	. . . . . . . 8 |- ( ( F e. ( C CovMap J ) /\ ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) /\ ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) ) ) -> ( ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) /\ ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) )
106	17, 65, 81, 103, 105	syl13anc 1221	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) /\ ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) )
107	106	simpld 459	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) )
108	2	cvmshmeo 27294	. . . . . 6 |- ( ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) /\ ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) ) -> ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( C ↾t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) Homeo ( J ↾t ( 1st ` ( T ` M ) ) ) ) )
109	65, 107, 108	syl2anc 661	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( C ↾t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) Homeo ( J ↾t ( 1st ` ( T ` M ) ) ) ) )
110		hmeocnvcn 19450	. . . . 5 |- ( ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( C ↾t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) Homeo ( J ↾t ( 1st ` ( T ` M ) ) ) ) -> `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( J ↾t ( 1st ` ( T ` M ) ) ) Cn ( C ↾t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) )
111	109, 110	syl 16	. . . 4 |- ( ( ph /\ M e. ( 1 ... N ) ) -> `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( J ↾t ( 1st ` ( T ` M ) ) ) Cn ( C ↾t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) )
112	28, 72, 111	cnmpt11f 19353	. . 3 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) e. ( ( L ↾t W ) Cn ( C ↾t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) )
113	20, 112	sseldd 3455	. 2 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) e. ( ( L ↾t W ) Cn C ) )
114	16, 113	eqeltrd 2539	1 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) e. ( ( L ↾t W ) Cn C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   A.wral 2795   {crab 2799   _Vcvv 3068   \ cdif 3423   u. cun 3424   i^i cin 3425   C_ wss 3426   (/)c0 3735   ~Pcpw 3958   {csn 3975   <.cop 3981   U.cuni 4189   U_ciun 4269   class class class wbr 4390   |-> cmpt 4448   _I cid 4729   X. cxp 4936   `'ccnv 4937   ran crn 4939   |` cres 4940   "cima 4941   Fn wfn 5511   -->wf 5512   ` cfv 5516   iota_crio 6150  (class class class)co 6190   |-> cmpt2 6192   1stc1st 6675   2ndc2nd 6676   RRcr 9382   0cc0 9383   1c1 9384   RR*cxr 9518   < clt 9519   <_ cle 9520   - cmin 9696   / cdiv 10094   NNcn 10423   (,)cioo 11401   [,]cicc 11404   ...cfz 11538   seqcseq 11907   ↾_t crest 14461   topGenctg 14478   Topctop 18614  TopOnctopon 18615   Cn ccn 18944   Homeochmeo 19442   IIcii 20567   CovMap ccvm 27278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4501  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460  ax-pre-sup 9461

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-int 4227  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-om 6577  df-1st 6677  df-2nd 6678  df-recs 6932  df-rdg 6966  df-oadd 7024  df-er 7201  df-map 7316  df-en 7411  df-dom 7412  df-sdom 7413  df-fin 7414  df-fi 7762  df-sup 7792  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-div 10095  df-nn 10424  df-2 10481  df-3 10482  df-n0 10681  df-z 10748  df-uz 10963  df-q 11055  df-rp 11093  df-xneg 11190  df-xadd 11191  df-xmul 11192  df-ioo 11405  df-icc 11408  df-fz 11539  df-seq 11908  df-exp 11967  df-cj 12690  df-re 12691  df-im 12692  df-sqr 12826  df-abs 12827  df-rest 14463  df-topgen 14484  df-psmet 17918  df-xmet 17919  df-met 17920  df-bl 17921  df-mopn 17922  df-top 18619  df-bases 18621  df-topon 18622  df-cn 18947  df-hmeo 19444  df-ii 20569  df-cvm 27279

This theorem is referenced by:  cvmliftlem10  27317