Metamath Proof Explorer

Theorem cvmliftlem3

Description: Lemma for cvmlift . Since 1st( TM ) is a neighborhood of ( G " W ) , every element A e. W satisfies ( GA ) e. ( 1st( TM ) ) . (Contributed by Mario Carneiro, 16-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 ) )
cvmliftlem3.3 
|- W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
cvmliftlem3.m 
|- ( ( ph /\ ps ) -> A e. W )
Assertion cvmliftlem3 
|- ( ( ph /\ ps ) -> ( G ` A ) e. ( 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 cvmliftlem3.3 
 |-  W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
14 cvmliftlem3.m 
 |-  ( ( ph /\ ps ) -> A e. W )
15 10 adantr 
 |-  ( ( ph /\ ps ) -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
16 oveq1 
 |-  ( k = M -> ( k - 1 ) = ( M - 1 ) )
17 16 oveq1d 
 |-  ( k = M -> ( ( k - 1 ) / N ) = ( ( M - 1 ) / N ) )
18 oveq1 
 |-  ( k = M -> ( k / N ) = ( M / N ) )
19 17 18 oveq12d 
 |-  ( k = M -> ( ( ( k - 1 ) / N ) [,] ( k / N ) ) = ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
20 19 13 eqtr4di 
 |-  ( k = M -> ( ( ( k - 1 ) / N ) [,] ( k / N ) ) = W )
21 20 imaeq2d 
 |-  ( k = M -> ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) = ( G " W ) )
22 2fveq3 
 |-  ( k = M -> ( 1st ` ( T ` k ) ) = ( 1st ` ( T ` M ) ) )
23 21 22 sseq12d 
 |-  ( k = M -> ( ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) <-> ( G " W ) C_ ( 1st ` ( T ` M ) ) ) )
24 23 rspcv 
 |-  ( M e. ( 1 ... N ) -> ( A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) -> ( G " W ) C_ ( 1st ` ( T ` M ) ) ) )
25 12 15 24 sylc 
 |-  ( ( ph /\ ps ) -> ( G " W ) C_ ( 1st ` ( T ` M ) ) )
26 iiuni 
 |-  ( 0 [,] 1 ) = U. II
27 26 3 cnf 
 |-  ( G e. ( II Cn J ) -> G : ( 0 [,] 1 ) --> X )
28 5 27 syl 
 |-  ( ph -> G : ( 0 [,] 1 ) --> X )
29 28 adantr 
 |-  ( ( ph /\ ps ) -> G : ( 0 [,] 1 ) --> X )
30 29 ffund 
 |-  ( ( ph /\ ps ) -> Fun G )
31 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem2 
 |-  ( ( ph /\ ps ) -> W C_ ( 0 [,] 1 ) )
32 29 fdmd 
 |-  ( ( ph /\ ps ) -> dom G = ( 0 [,] 1 ) )
33 31 32 sseqtrrd 
 |-  ( ( ph /\ ps ) -> W C_ dom G )
34 funfvima2 
 |-  ( ( Fun G /\ W C_ dom G ) -> ( A e. W -> ( G ` A ) e. ( G " W ) ) )
35 30 33 34 syl2anc 
 |-  ( ( ph /\ ps ) -> ( A e. W -> ( G ` A ) e. ( G " W ) ) )
36 14 35 mpd 
 |-  ( ( ph /\ ps ) -> ( G ` A ) e. ( G " W ) )
37 25 36 sseldd 
 |-  ( ( ph /\ ps ) -> ( G ` A ) e. ( 1st ` ( T ` M ) ) )