Theorem cvmliftlem8 27029

Description: Lemma for cvmlift 27036. 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 11465	. . 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 27026	. . 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 471	. 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 462	. . . 4 |- ( ( ph /\ M e. ( 1 ... N ) ) -> F e. ( C CovMap J ) )
18		cvmtop1 26997	. . . 4 |- ( F e. ( C CovMap J ) -> C e. Top )
19		cnrest2r 18733	. . . 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 20184	. . . . . 6 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
22	12, 21	eqeltri 2503	. . . . 5 |- L e. (TopOn ` RR )
23		simpr 458	. . . . . . 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 27023	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ ( 0 [,] 1 ) )
25		unitssre 11419	. . . . . 6 |- ( 0 [,] 1 ) C_ RR
26	24, 25	syl6ss 3356	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ RR )
27		resttopon 18607	. . . . 5 |- ( ( L e. (TopOn ` RR ) /\ W C_ RR ) -> ( L ↾t W ) e. (TopOn ` W ) )
28	22, 26, 27	sylancr 656	. . . 4 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( L ↾t W ) e. (TopOn ` W ) )
29		eqid 2433	. . . . . . 7 |- ( II ↾t W ) = ( II ↾t W )
30		iitopon 20297	. . . . . . . 8 |- II e. (TopOn ` ( 0 [,] 1 ) )
31	30	a1i 11	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> II e. (TopOn ` ( 0 [,] 1 ) ) )
32	6	adantr 462	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G e. ( II Cn J ) )
33		iiuni 20299	. . . . . . . . . . 11 |- ( 0 [,] 1 ) = U. II
34	33, 4	cnf 18692	. . . . . . . . . 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 5732	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G = ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) )
37	36, 32	eqeltrrd 2508	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) e. ( II Cn J ) )
38	29, 31, 24, 37	cnmpt1res 19091	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( II ↾t W ) Cn J ) )
39		dfii2 20300	. . . . . . . . . 10 |- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
40	12	oveq1i 6090	. . . . . . . . . 10 |- ( L ↾t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
41	39, 40	eqtr4i 2456	. . . . . . . . 9 |- II = ( L ↾t ( 0 [,] 1 ) )
42	41	oveq1i 6090	. . . . . . . 8 |- ( II ↾t W ) = ( ( L ↾t ( 0 [,] 1 ) ) ↾t W )
43		retop 20182	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) e. Top
44	12, 43	eqeltri 2503	. . . . . . . . . 10 |- L e. Top
45	44	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> L e. Top )
46		ovex 6105	. . . . . . . . . 10 |- ( 0 [,] 1 ) e. _V
47	46	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 0 [,] 1 ) e. _V )
48		restabs 18611	. . . . . . . . 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 1211	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( L ↾t ( 0 [,] 1 ) ) ↾t W ) = ( L ↾t W ) )
50	42, 49	syl5eq 2477	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( II ↾t W ) = ( L ↾t W ) )
51	50	oveq1d 6095	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( II ↾t W ) Cn J ) = ( ( L ↾t W ) Cn J ) )
52	38, 51	eleqtrd 2509	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn J ) )
53		cvmtop2 26998	. . . . . . . 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 18380	. . . . . . 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 748	. . . . . . . . . 10 |- ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> M e. ( 1 ... N ) )
58		simprr 749	. . . . . . . . . 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 27024	. . . . . . . . 9 |- ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
60	59	anassrs 641	. . . . . . . 8 |- ( ( ( ph /\ M e. ( 1 ... N ) ) /\ z e. W ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
61		eqid 2433	. . . . . . . 8 |- ( z e. W |-> ( G ` z ) ) = ( z e. W |-> ( G ` z ) )
62	60, 61	fmptd 5855	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) : W --> ( 1st ` ( T ` M ) ) )
63		frn 5553	. . . . . . 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 27022	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
66	2	cvmsrcl 27001	. . . . . . . 8 |- ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) -> ( 1st ` ( T ` M ) ) e. J )
67		elssuni 4109	. . . . . . . 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 3391	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ X )
70		cnrest2 18732	. . . . . 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 1211	. . . . 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 27028	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
74		cvmcn 26999	. . . . . . . . . . . 12 |- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
75	3, 4	cnf 18692	. . . . . . . . . . . 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 5547	. . . . . . . . . . 11 |- ( F : B --> X -> F Fn B )
78		fniniseg 5812	. . . . . . . . . . 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 456	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B )
82	80	simprd 460	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) )
83	1	adantl 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. NN )
84	83	nnred 10325	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. RR )
85		peano2rem 9663	. . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> N e. NN )
88	86, 87	nndivred 10358	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR )
89	88	rexrd 9421	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR* )
90	84, 87	nndivred 10358	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR )
91	90	rexrd 9421	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR* )
92	84	ltm1d 10253	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) < M )
93	87	nnred 10325	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> N e. RR )
94	87	nngt0d 10353	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> 0 < N )
95		ltdiv1 10181	. . . . . . . . . . . . . . 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 1215	. . . . . . . . . . . . . 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 9510	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) <_ ( M / N ) )
99		lbicc2 11388	. . . . . . . . . . . 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 1211	. . . . . . . . . . 11 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
101	100, 14	syl6eleqr 2524	. . . . . . . . . 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 27024	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( G ` ( ( M - 1 ) / N ) ) e. ( 1st ` ( T ` M ) ) )
103	82, 102	eqeltrd 2507	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) )
104		eqid 2433	. . . . . . . . 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 27014	. . . . . . . 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 1213	. . . . . . 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 456	. . . . . 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 27008	. . . . . 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 654	. . . . 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 19176	. . . . 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 19079	. . 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 3345	. 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 2507	1 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) e. ( ( L ↾t W ) Cn C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   A.wral 2705   {crab 2709   _Vcvv 2962   \ cdif 3313   u. cun 3314   i^i cin 3315   C_ wss 3316   (/)c0 3625   ~Pcpw 3848   {csn 3865   <.cop 3871   U.cuni 4079   U_ciun 4159   class class class wbr 4280   e. cmpt 4338   _I cid 4618   X. cxp 4825   `'ccnv 4826   ran crn 4828   |` cres 4829   "cima 4830   Fn wfn 5401   -->wf 5402   ` cfv 5406   iota_crio 6038  (class class class)co 6080   e. cmpt2 6082   1stc1st 6564   2ndc2nd 6565   RRcr 9269   0cc0 9270   1c1 9271   RR*cxr 9405   < clt 9406   <_ cle 9407   - cmin 9583   / cdiv 9981   NNcn 10310   (,)cioo 11288   [,]cicc 11291   ...cfz 11424   seqcseq 11790   ↾_t crest 14342   topGenctg 14359   Topctop 18340  TopOnctopon 18341   Cn ccn 18670   Homeochmeo 19168   IIcii 20293   CovMap ccvm 26992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-oadd 6912  df-er 7089  df-map 7204  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fi 7649  df-sup 7679  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-n0 10568  df-z 10635  df-uz 10850  df-q 10942  df-rp 10980  df-xneg 11077  df-xadd 11078  df-xmul 11079  df-ioo 11292  df-icc 11295  df-fz 11425  df-seq 11791  df-exp 11850  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-rest 14344  df-topgen 14365  df-psmet 17653  df-xmet 17654  df-met 17655  df-bl 17656  df-mopn 17657  df-top 18345  df-bases 18347  df-topon 18348  df-cn 18673  df-hmeo 19170  df-ii 20295  df-cvm 26993

This theorem is referenced by:  cvmliftlem10  27031