Theorem cvmliftlem8 27150

Description: Lemma for cvmlift 27157. 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 11470	. . 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 27147	. . 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 27118	. . . 4 |- ( F e. ( C CovMap J ) -> C e. Top )
19		cnrest2r 18871	. . . 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 20322	. . . . . 6 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
22	12, 21	eqeltri 2508	. . . . 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 27144	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ ( 0 [,] 1 ) )
25		unitssre 11424	. . . . . 6 |- ( 0 [,] 1 ) C_ RR
26	24, 25	syl6ss 3363	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ RR )
27		resttopon 18745	. . . . 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 2438	. . . . . . 7 |- ( II ↾t W ) = ( II ↾t W )
30		iitopon 20435	. . . . . . . 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 20437	. . . . . . . . . . 11 |- ( 0 [,] 1 ) = U. II
34	33, 4	cnf 18830	. . . . . . . . . 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 5739	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G = ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) )
37	36, 32	eqeltrrd 2513	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) e. ( II Cn J ) )
38	29, 31, 24, 37	cnmpt1res 19229	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( II ↾t W ) Cn J ) )
39		dfii2 20438	. . . . . . . . . 10 |- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
40	12	oveq1i 6096	. . . . . . . . . 10 |- ( L ↾t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
41	39, 40	eqtr4i 2461	. . . . . . . . 9 |- II = ( L ↾t ( 0 [,] 1 ) )
42	41	oveq1i 6096	. . . . . . . 8 |- ( II ↾t W ) = ( ( L ↾t ( 0 [,] 1 ) ) ↾t W )
43		retop 20320	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) e. Top
44	12, 43	eqeltri 2508	. . . . . . . . . 10 |- L e. Top
45	44	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> L e. Top )
46		ovex 6111	. . . . . . . . . 10 |- ( 0 [,] 1 ) e. _V
47	46	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 0 [,] 1 ) e. _V )
48		restabs 18749	. . . . . . . . 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 1218	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( L ↾t ( 0 [,] 1 ) ) ↾t W ) = ( L ↾t W ) )
50	42, 49	syl5eq 2482	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( II ↾t W ) = ( L ↾t W ) )
51	50	oveq1d 6101	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( II ↾t W ) Cn J ) = ( ( L ↾t W ) Cn J ) )
52	38, 51	eleqtrd 2514	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn J ) )
53		cvmtop2 27119	. . . . . . . 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 18518	. . . . . . 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 27145	. . . . . . . . 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 2438	. . . . . . . 8 |- ( z e. W |-> ( G ` z ) ) = ( z e. W |-> ( G ` z ) )
62	60, 61	fmptd 5862	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) : W --> ( 1st ` ( T ` M ) ) )
63		frn 5560	. . . . . . 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 27143	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
66	2	cvmsrcl 27122	. . . . . . . 8 |- ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) -> ( 1st ` ( T ` M ) ) e. J )
67		elssuni 4116	. . . . . . . 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 3398	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ X )
70		cnrest2 18870	. . . . . 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 1218	. . . . 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 27149	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
74		cvmcn 27120	. . . . . . . . . . . 12 |- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
75	3, 4	cnf 18830	. . . . . . . . . . . 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 5554	. . . . . . . . . . 11 |- ( F : B --> X -> F Fn B )
78		fniniseg 5819	. . . . . . . . . . 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 10329	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. RR )
85		peano2rem 9667	. . . . . . . . . . . . . . 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 10362	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR )
89	88	rexrd 9425	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR* )
90	84, 87	nndivred 10362	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR )
91	90	rexrd 9425	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR* )
92	84	ltm1d 10257	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) < M )
93	87	nnred 10329	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> N e. RR )
94	87	nngt0d 10357	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> 0 < N )
95		ltdiv1 10185	. . . . . . . . . . . . . . 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 1222	. . . . . . . . . . . . . 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 9514	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) <_ ( M / N ) )
99		lbicc2 11393	. . . . . . . . . . . 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 1218	. . . . . . . . . . 11 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
101	100, 14	syl6eleqr 2529	. . . . . . . . . 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 27145	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( G ` ( ( M - 1 ) / N ) ) e. ( 1st ` ( T ` M ) ) )
103	82, 102	eqeltrd 2512	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) )
104		eqid 2438	. . . . . . . . 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 27135	. . . . . . . 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 1220	. . . . . . 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 27129	. . . . . 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 19314	. . . . 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 19217	. . 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 3352	. 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 2512	1 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) e. ( ( L ↾t W ) Cn C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2710   {crab 2714   _Vcvv 2967   \ cdif 3320   u. cun 3321   i^i cin 3322   C_ wss 3323   (/)c0 3632   ~Pcpw 3855   {csn 3872   <.cop 3878   U.cuni 4086   U_ciun 4166   class class class wbr 4287   e. cmpt 4345   _I cid 4626   X. cxp 4833   `'ccnv 4834   ran crn 4836   |` cres 4837   "cima 4838   Fn wfn 5408   -->wf 5409   ` cfv 5413   iota_crio 6046  (class class class)co 6086   e. cmpt2 6088   1stc1st 6570   2ndc2nd 6571   RRcr 9273   0cc0 9274   1c1 9275   RR*cxr 9409   < clt 9410   <_ cle 9411   - cmin 9587   / cdiv 9985   NNcn 10314   (,)cioo 11292   [,]cicc 11295   ...cfz 11429   seqcseq 11798   ↾_t crest 14351   topGenctg 14368   Topctop 18478  TopOnctopon 18479   Cn ccn 18808   Homeochmeo 19306   IIcii 20431   CovMap ccvm 27113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-oadd 6916  df-er 7093  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fi 7653  df-sup 7683  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-n0 10572  df-z 10639  df-uz 10854  df-q 10946  df-rp 10984  df-xneg 11081  df-xadd 11082  df-xmul 11083  df-ioo 11296  df-icc 11299  df-fz 11430  df-seq 11799  df-exp 11858  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-rest 14353  df-topgen 14374  df-psmet 17789  df-xmet 17790  df-met 17791  df-bl 17792  df-mopn 17793  df-top 18483  df-bases 18485  df-topon 18486  df-cn 18811  df-hmeo 19308  df-ii 20433  df-cvm 27114

This theorem is referenced by:  cvmliftlem10  27152