Theorem cvmliftlem1

Description: Lemma for cvmlift . In cvmliftlem15 , we picked an N large enough so that the sections ( G " [ ( k - 1 ) / N , k / N ] ) are all contained in an even covering, and the function T enumerates these even coverings. So 1st( TM ) is a neighborhood of ( G " [ ( M - 1 ) / N , M / N ] ) , and 2nd( TM ) is an even covering of 1st( TM ) , which is to say a disjoint union of open sets in C whose image is 1st( TM ) . (Contributed by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypotheses	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 (,) )
	cvmliftlem1.m	|- ( ( ph /\ ps ) -> M e. ( 1 ... N ) )
Assertion	cvmliftlem1	|- ( ( ph /\ ps ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		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 ) ) ) ) } )
2		cvmliftlem.b	|- B = U. C
3		cvmliftlem.x	|- X = U. J
4		cvmliftlem.f	|- ( ph -> F e. ( C CovMap J ) )
5		cvmliftlem.g	|- ( ph -> G e. ( II Cn J ) )
6		cvmliftlem.p	|- ( ph -> P e. B )
7		cvmliftlem.e	|- ( ph -> ( F ` P ) = ( G ` 0 ) )
8		cvmliftlem.n	|- ( ph -> N e. NN )
9		cvmliftlem.t	|- ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
10		cvmliftlem.a	|- ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
11		cvmliftlem.l	|- L = ( topGen ` ran (,) )
12		cvmliftlem1.m	|- ( ( ph /\ ps ) -> M e. ( 1 ... N ) )
13		relxp	|- Rel ( { j } X. ( S ` j ) )
14	13	rgenw	|- A. j e. J Rel ( { j } X. ( S ` j ) )
15		reliun	|- ( Rel U_ j e. J ( { j } X. ( S ` j ) ) <-> A. j e. J Rel ( { j } X. ( S ` j ) ) )
16	14 15	mpbir	|- Rel U_ j e. J ( { j } X. ( S ` j ) )
17	9	adantr	|- ( ( ph /\ ps ) -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
18	17 12	ffvelrnd	|- ( ( ph /\ ps ) -> ( T ` M ) e. U_ j e. J ( { j } X. ( S ` j ) ) )
19		1st2nd	|- ( ( Rel U_ j e. J ( { j } X. ( S ` j ) ) /\ ( T ` M ) e. U_ j e. J ( { j } X. ( S ` j ) ) ) -> ( T ` M ) = <. ( 1st ` ( T ` M ) ) , ( 2nd ` ( T ` M ) ) >. )
20	16 18 19	sylancr	|- ( ( ph /\ ps ) -> ( T ` M ) = <. ( 1st ` ( T ` M ) ) , ( 2nd ` ( T ` M ) ) >. )
21	20 18	eqeltrrd	|- ( ( ph /\ ps ) -> <. ( 1st ` ( T ` M ) ) , ( 2nd ` ( T ` M ) ) >. e. U_ j e. J ( { j } X. ( S ` j ) ) )
22		fveq2	|- ( j = ( 1st ` ( T ` M ) ) -> ( S ` j ) = ( S ` ( 1st ` ( T ` M ) ) ) )
23	22	opeliunxp2	|- ( <. ( 1st ` ( T ` M ) ) , ( 2nd ` ( T ` M ) ) >. e. U_ j e. J ( { j } X. ( S ` j ) ) <-> ( ( 1st ` ( T ` M ) ) e. J /\ ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) ) )
24	23	simprbi	|- ( <. ( 1st ` ( T ` M ) ) , ( 2nd ` ( T ` M ) ) >. e. U_ j e. J ( { j } X. ( S ` j ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
25	21 24	syl	|- ( ( ph /\ ps ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )