Theorem cvmliftlem8 28227

Description: Lemma for cvmlift 28234. 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 11703	. . 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 28224	. . 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 28195	. . . 4 |- ( F e. ( C CovMap J ) -> C e. Top )
19		cnrest2r 19547	. . . 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 20998	. . . . . 6 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
22	12, 21	eqeltri 2544	. . . . 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 28221	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ ( 0 [,] 1 ) )
25		unitssre 11656	. . . . . 6 |- ( 0 [,] 1 ) C_ RR
26	24, 25	syl6ss 3509	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ RR )
27		resttopon 19421	. . . . 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 2460	. . . . . . 7 |- ( II ↾t W ) = ( II ↾t W )
30		iitopon 21111	. . . . . . . 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 21113	. . . . . . . . . . 11 |- ( 0 [,] 1 ) = U. II
34	33, 4	cnf 19506	. . . . . . . . . 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 5911	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G = ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) )
37	36, 32	eqeltrrd 2549	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) e. ( II Cn J ) )
38	29, 31, 24, 37	cnmpt1res 19905	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( II ↾t W ) Cn J ) )
39		dfii2 21114	. . . . . . . . . 10 |- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
40	12	oveq1i 6285	. . . . . . . . . 10 |- ( L ↾t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
41	39, 40	eqtr4i 2492	. . . . . . . . 9 |- II = ( L ↾t ( 0 [,] 1 ) )
42	41	oveq1i 6285	. . . . . . . 8 |- ( II ↾t W ) = ( ( L ↾t ( 0 [,] 1 ) ) ↾t W )
43		retop 20996	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) e. Top
44	12, 43	eqeltri 2544	. . . . . . . . . 10 |- L e. Top
45	44	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> L e. Top )
46		ovex 6300	. . . . . . . . . 10 |- ( 0 [,] 1 ) e. _V
47	46	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 0 [,] 1 ) e. _V )
48		restabs 19425	. . . . . . . . 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 1223	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( L ↾t ( 0 [,] 1 ) ) ↾t W ) = ( L ↾t W ) )
50	42, 49	syl5eq 2513	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( II ↾t W ) = ( L ↾t W ) )
51	50	oveq1d 6290	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( II ↾t W ) Cn J ) = ( ( L ↾t W ) Cn J ) )
52	38, 51	eleqtrd 2550	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn J ) )
53		cvmtop2 28196	. . . . . . . 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 19194	. . . . . . 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 28222	. . . . . . . . 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 2460	. . . . . . . 8 |- ( z e. W |-> ( G ` z ) ) = ( z e. W |-> ( G ` z ) )
62	60, 61	fmptd 6036	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) : W --> ( 1st ` ( T ` M ) ) )
63		frn 5728	. . . . . . 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 28220	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
66	2	cvmsrcl 28199	. . . . . . . 8 |- ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) -> ( 1st ` ( T ` M ) ) e. J )
67		elssuni 4268	. . . . . . . 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 3544	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ X )
70		cnrest2 19546	. . . . . 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 1223	. . . . 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 28226	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
74		cvmcn 28197	. . . . . . . . . . . 12 |- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
75	3, 4	cnf 19506	. . . . . . . . . . . 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 5722	. . . . . . . . . . 11 |- ( F : B --> X -> F Fn B )
78		fniniseg 5993	. . . . . . . . . . 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 10540	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. RR )
85		peano2rem 9875	. . . . . . . . . . . . . . 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 10573	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR )
89	88	rexrd 9632	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR* )
90	84, 87	nndivred 10573	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR )
91	90	rexrd 9632	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR* )
92	84	ltm1d 10467	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) < M )
93	87	nnred 10540	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> N e. RR )
94	87	nngt0d 10568	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> 0 < N )
95		ltdiv1 10395	. . . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . . 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 9721	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) <_ ( M / N ) )
99		lbicc2 11625	. . . . . . . . . . . 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 1223	. . . . . . . . . . 11 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
101	100, 14	syl6eleqr 2559	. . . . . . . . . 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 28222	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( G ` ( ( M - 1 ) / N ) ) e. ( 1st ` ( T ` M ) ) )
103	82, 102	eqeltrd 2548	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) )
104		eqid 2460	. . . . . . . . 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 28212	. . . . . . . 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 1225	. . . . . . 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 28206	. . . . . 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 19990	. . . . 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 19893	. . 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 3498	. 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 2548	1 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) e. ( ( L ↾t W ) Cn C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1374   e. wcel 1762   A.wral 2807   {crab 2811   _Vcvv 3106   \ cdif 3466   u. cun 3467   i^i cin 3468   C_ wss 3469   (/)c0 3778   ~Pcpw 4003   {csn 4020   <.cop 4026   U.cuni 4238   U_ciun 4318   class class class wbr 4440   |-> cmpt 4498   _I cid 4783   X. cxp 4990   `'ccnv 4991   ran crn 4993   |` cres 4994   "cima 4995   Fn wfn 5574   -->wf 5575   ` cfv 5579   iota_crio 6235  (class class class)co 6275   |-> cmpt2 6277   1stc1st 6772   2ndc2nd 6773   RRcr 9480   0cc0 9481   1c1 9482   RR*cxr 9616   < clt 9617   <_ cle 9618   - cmin 9794   / cdiv 10195   NNcn 10525   (,)cioo 11518   [,]cicc 11521   ...cfz 11661   seqcseq 12063   ↾_t crest 14665   topGenctg 14682   Topctop 19154  TopOnctopon 19155   Cn ccn 19484   Homeochmeo 19982   IIcii 21107   CovMap ccvm 28190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-int 4276  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6672  df-1st 6774  df-2nd 6775  df-recs 7032  df-rdg 7066  df-oadd 7124  df-er 7301  df-map 7412  df-en 7507  df-dom 7508  df-sdom 7509  df-fin 7510  df-fi 7860  df-sup 7890  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-div 10196  df-nn 10526  df-2 10583  df-3 10584  df-n0 10785  df-z 10854  df-uz 11072  df-q 11172  df-rp 11210  df-xneg 11307  df-xadd 11308  df-xmul 11309  df-ioo 11522  df-icc 11525  df-fz 11662  df-seq 12064  df-exp 12123  df-cj 12882  df-re 12883  df-im 12884  df-sqr 13018  df-abs 13019  df-rest 14667  df-topgen 14688  df-psmet 18175  df-xmet 18176  df-met 18177  df-bl 18178  df-mopn 18179  df-top 19159  df-bases 19161  df-topon 19162  df-cn 19487  df-hmeo 19984  df-ii 21109  df-cvm 28191

This theorem is referenced by:  cvmliftlem10  28229