Theorem cvmliftlem8 29589

Description: Lemma for cvmlift 29596. 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 11768	. . 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 29586	. . 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 472	. 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 463	. . . 4 |- ( ( ph /\ M e. ( 1 ... N ) ) -> F e. ( C CovMap J ) )
18		cvmtop1 29557	. . . 4 |- ( F e. ( C CovMap J ) -> C e. Top )
19		cnrest2r 20081	. . . 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 18	. . 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 21562	. . . . . 6 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
22	12, 21	eqeltri 2486	. . . . 5 |- L e. (TopOn ` RR )
23		simpr 459	. . . . . . 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 29583	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ ( 0 [,] 1 ) )
25		unitssre 11721	. . . . . 6 |- ( 0 [,] 1 ) C_ RR
26	24, 25	syl6ss 3454	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ RR )
27		resttopon 19955	. . . . 5 |- ( ( L e. (TopOn ` RR ) /\ W C_ RR ) -> ( L ↾t W ) e. (TopOn ` W ) )
28	22, 26, 27	sylancr 661	. . . 4 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( L ↾t W ) e. (TopOn ` W ) )
29		eqid 2402	. . . . . . 7 |- ( II ↾t W ) = ( II ↾t W )
30		iitopon 21675	. . . . . . . 8 |- II e. (TopOn ` ( 0 [,] 1 ) )
31	30	a1i 11	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> II e. (TopOn ` ( 0 [,] 1 ) ) )
32	6	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G e. ( II Cn J ) )
33		iiuni 21677	. . . . . . . . . . 11 |- ( 0 [,] 1 ) = U. II
34	33, 4	cnf 20040	. . . . . . . . . 10 |- ( G e. ( II Cn J ) -> G : ( 0 [,] 1 ) --> X )
35	32, 34	syl 17	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G : ( 0 [,] 1 ) --> X )
36	35	feqmptd 5902	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> G = ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) )
37	36, 32	eqeltrrd 2491	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) e. ( II Cn J ) )
38	29, 31, 24, 37	cnmpt1res 20469	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( II ↾t W ) Cn J ) )
39		dfii2 21678	. . . . . . . . . 10 |- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
40	12	oveq1i 6288	. . . . . . . . . 10 |- ( L ↾t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
41	39, 40	eqtr4i 2434	. . . . . . . . 9 |- II = ( L ↾t ( 0 [,] 1 ) )
42	41	oveq1i 6288	. . . . . . . 8 |- ( II ↾t W ) = ( ( L ↾t ( 0 [,] 1 ) ) ↾t W )
43		retop 21560	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) e. Top
44	12, 43	eqeltri 2486	. . . . . . . . . 10 |- L e. Top
45	44	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> L e. Top )
46		ovex 6306	. . . . . . . . . 10 |- ( 0 [,] 1 ) e. _V
47	46	a1i 11	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 0 [,] 1 ) e. _V )
48		restabs 19959	. . . . . . . . 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 1230	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( L ↾t ( 0 [,] 1 ) ) ↾t W ) = ( L ↾t W ) )
50	42, 49	syl5eq 2455	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( II ↾t W ) = ( L ↾t W ) )
51	50	oveq1d 6293	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( II ↾t W ) Cn J ) = ( ( L ↾t W ) Cn J ) )
52	38, 51	eleqtrd 2492	. . . . 5 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( L ↾t W ) Cn J ) )
53		cvmtop2 29558	. . . . . . . 8 |- ( F e. ( C CovMap J ) -> J e. Top )
54	17, 53	syl 17	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> J e. Top )
55	4	toptopon 19726	. . . . . . 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 756	. . . . . . . . . 10 |- ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> M e. ( 1 ... N ) )
58		simprr 758	. . . . . . . . . 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 29584	. . . . . . . . 9 |- ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
60	59	anassrs 646	. . . . . . . 8 |- ( ( ( ph /\ M e. ( 1 ... N ) ) /\ z e. W ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
61		eqid 2402	. . . . . . . 8 |- ( z e. W |-> ( G ` z ) ) = ( z e. W |-> ( G ` z ) )
62	60, 61	fmptd 6033	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) : W --> ( 1st ` ( T ` M ) ) )
63		frn 5720	. . . . . . 7 |- ( ( z e. W |-> ( G ` z ) ) : W --> ( 1st ` ( T ` M ) ) -> ran ( z e. W |-> ( G ` z ) ) C_ ( 1st ` ( T ` M ) ) )
64	62, 63	syl 17	. . . . . 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 29582	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
66	2	cvmsrcl 29561	. . . . . . . 8 |- ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) -> ( 1st ` ( T ` M ) ) e. J )
67		elssuni 4220	. . . . . . . 8 |- ( ( 1st ` ( T ` M ) ) e. J -> ( 1st ` ( T ` M ) ) C_ U. J )
68	65, 66, 67	3syl 18	. . . . . . 7 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ U. J )
69	68, 4	syl6sseqr 3489	. . . . . 6 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ X )
70		cnrest2 20080	. . . . . 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 1230	. . . . 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 29588	. . . . . . . . . 10 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
74		cvmcn 29559	. . . . . . . . . . . 12 |- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
75	3, 4	cnf 20040	. . . . . . . . . . . 12 |- ( F e. ( C Cn J ) -> F : B --> X )
76	17, 74, 75	3syl 18	. . . . . . . . . . 11 |- ( ( ph /\ M e. ( 1 ... N ) ) -> F : B --> X )
77		ffn 5714	. . . . . . . . . . 11 |- ( F : B --> X -> F Fn B )
78		fniniseg 5986	. . . . . . . . . . 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 18	. . . . . . . . . 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 457	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B )
82	80	simprd 461	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) )
83	1	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. NN )
84	83	nnred 10591	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> M e. RR )
85		peano2rem 9922	. . . . . . . . . . . . . . 15 |- ( M e. RR -> ( M - 1 ) e. RR )
86	84, 85	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) e. RR )
87	9	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> N e. NN )
88	86, 87	nndivred 10625	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR )
89	88	rexrd 9673	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR* )
90	84, 87	nndivred 10625	. . . . . . . . . . . . 13 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR )
91	90	rexrd 9673	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR* )
92	84	ltm1d 10518	. . . . . . . . . . . . . 14 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) < M )
93	87	nnred 10591	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> N e. RR )
94	87	nngt0d 10620	. . . . . . . . . . . . . . 15 |- ( ( ph /\ M e. ( 1 ... N ) ) -> 0 < N )
95		ltdiv1 10447	. . . . . . . . . . . . . . 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 1234	. . . . . . . . . . . . . 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 9765	. . . . . . . . . . . 12 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) <_ ( M / N ) )
99		lbicc2 11690	. . . . . . . . . . . 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 1230	. . . . . . . . . . 11 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
101	100, 14	syl6eleqr 2501	. . . . . . . . . 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 29584	. . . . . . . . 9 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( G ` ( ( M - 1 ) / N ) ) e. ( 1st ` ( T ` M ) ) )
103	82, 102	eqeltrd 2490	. . . . . . . 8 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) )
104		eqid 2402	. . . . . . . . 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 29574	. . . . . . . 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 1232	. . . . . . 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 457	. . . . . 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 29568	. . . . . 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 659	. . . . 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 20554	. . . . 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 17	. . . 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 20457	. . 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 3443	. 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 2490	1 |- ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) e. ( ( L ↾t W ) Cn C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1405   e. wcel 1842   A.wral 2754   {crab 2758   _Vcvv 3059   \ cdif 3411   u. cun 3412   i^i cin 3413   C_ wss 3414   (/)c0 3738   ~Pcpw 3955   {csn 3972   <.cop 3978   U.cuni 4191   U_ciun 4271   class class class wbr 4395   |-> cmpt 4453   _I cid 4733   X. cxp 4821   `'ccnv 4822   ran crn 4824   |` cres 4825   "cima 4826   Fn wfn 5564   -->wf 5565   ` cfv 5569   iota_crio 6239  (class class class)co 6278   |-> cmpt2 6280   1stc1st 6782   2ndc2nd 6783   RRcr 9521   0cc0 9522   1c1 9523   RR*cxr 9657   < clt 9658   <_ cle 9659   - cmin 9841   / cdiv 10247   NNcn 10576   (,)cioo 11582   [,]cicc 11585   ...cfz 11726   seqcseq 12151   ↾_t crest 15035   topGenctg 15052   Topctop 19686  TopOnctopon 19687   Cn ccn 20018   Homeochmeo 20546   IIcii 21671   CovMap ccvm 29552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599  ax-pre-sup 9600

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6684  df-1st 6784  df-2nd 6785  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-oadd 7171  df-er 7348  df-map 7459  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558  df-fi 7905  df-sup 7935  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-div 10248  df-nn 10577  df-2 10635  df-3 10636  df-n0 10837  df-z 10906  df-uz 11128  df-q 11228  df-rp 11266  df-xneg 11371  df-xadd 11372  df-xmul 11373  df-ioo 11586  df-icc 11589  df-fz 11727  df-seq 12152  df-exp 12211  df-cj 13081  df-re 13082  df-im 13083  df-sqrt 13217  df-abs 13218  df-rest 15037  df-topgen 15058  df-psmet 18731  df-xmet 18732  df-met 18733  df-bl 18734  df-mopn 18735  df-top 19691  df-bases 19693  df-topon 19694  df-cn 20021  df-hmeo 20548  df-ii 21673  df-cvm 29553

This theorem is referenced by:  cvmliftlem10  29591