Metamath Proof Explorer

Theorem cvmlift2lem9a

Description: Lemma for cvmlift2 and cvmlift3 . (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses cvmlift2lem9a.b 
|- B = U. C
cvmlift2lem9a.y 
|- Y = U. K
cvmlift2lem9a.s 
|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. c e. s ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) } )
cvmlift2lem9a.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift2lem9a.h 
|- ( ph -> H : Y --> B )
cvmlift2lem9a.g 
|- ( ph -> ( F o. H ) e. ( K Cn J ) )
cvmlift2lem9a.k 
|- ( ph -> K e. Top )
cvmlift2lem9a.1 
|- ( ph -> X e. Y )
cvmlift2lem9a.2 
|- ( ph -> T e. ( S ` A ) )
cvmlift2lem9a.3 
|- ( ph -> ( W e. T /\ ( H ` X ) e. W ) )
cvmlift2lem9a.4 
|- ( ph -> M C_ Y )
cvmlift2lem9a.6 
|- ( ph -> ( H " M ) C_ W )
Assertion cvmlift2lem9a 
|- ( ph -> ( H |` M ) e. ( ( K |`t M ) Cn C ) )

Proof

Step Hyp Ref Expression
1 cvmlift2lem9a.b 
 |-  B = U. C
2 cvmlift2lem9a.y 
 |-  Y = U. K
3 cvmlift2lem9a.s 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. c e. s ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) } )
4 cvmlift2lem9a.f 
 |-  ( ph -> F e. ( C CovMap J ) )
5 cvmlift2lem9a.h 
 |-  ( ph -> H : Y --> B )
6 cvmlift2lem9a.g 
 |-  ( ph -> ( F o. H ) e. ( K Cn J ) )
7 cvmlift2lem9a.k 
 |-  ( ph -> K e. Top )
8 cvmlift2lem9a.1 
 |-  ( ph -> X e. Y )
9 cvmlift2lem9a.2 
 |-  ( ph -> T e. ( S ` A ) )
10 cvmlift2lem9a.3 
 |-  ( ph -> ( W e. T /\ ( H ` X ) e. W ) )
11 cvmlift2lem9a.4 
 |-  ( ph -> M C_ Y )
12 cvmlift2lem9a.6 
 |-  ( ph -> ( H " M ) C_ W )
13 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
14 4 13 syl 
 |-  ( ph -> C e. Top )
15 cnrest2r 
 |-  ( C e. Top -> ( ( K |`t M ) Cn ( C |`t W ) ) C_ ( ( K |`t M ) Cn C ) )
16 14 15 syl 
 |-  ( ph -> ( ( K |`t M ) Cn ( C |`t W ) ) C_ ( ( K |`t M ) Cn C ) )
17 5 ffnd 
 |-  ( ph -> H Fn Y )
18 fnssres 
 |-  ( ( H Fn Y /\ M C_ Y ) -> ( H |` M ) Fn M )
19 17 11 18 syl2anc 
 |-  ( ph -> ( H |` M ) Fn M )
20 df-ima 
 |-  ( H " M ) = ran ( H |` M )
21 20 12 eqsstrrid 
 |-  ( ph -> ran ( H |` M ) C_ W )
22 df-f 
 |-  ( ( H |` M ) : M --> W <-> ( ( H |` M ) Fn M /\ ran ( H |` M ) C_ W ) )
23 19 21 22 sylanbrc 
 |-  ( ph -> ( H |` M ) : M --> W )
24 10 simpld 
 |-  ( ph -> W e. T )
25 3 cvmsf1o 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` A ) /\ W e. T ) -> ( F |` W ) : W -1-1-onto-> A )
26 4 9 24 25 syl3anc 
 |-  ( ph -> ( F |` W ) : W -1-1-onto-> A )
27 26 adantr 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( F |` W ) : W -1-1-onto-> A )
28 f1of1 
 |-  ( ( F |` W ) : W -1-1-onto-> A -> ( F |` W ) : W -1-1-> A )
29 27 28 syl 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( F |` W ) : W -1-1-> A )
30 1 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` B ) )
31 14 30 sylib 
 |-  ( ph -> C e. ( TopOn ` B ) )
32 3 cvmsss 
 |-  ( T e. ( S ` A ) -> T C_ C )
33 9 32 syl 
 |-  ( ph -> T C_ C )
34 33 24 sseldd 
 |-  ( ph -> W e. C )
35 toponss 
 |-  ( ( C e. ( TopOn ` B ) /\ W e. C ) -> W C_ B )
36 31 34 35 syl2anc 
 |-  ( ph -> W C_ B )
37 resttopon 
 |-  ( ( C e. ( TopOn ` B ) /\ W C_ B ) -> ( C |`t W ) e. ( TopOn ` W ) )
38 31 36 37 syl2anc 
 |-  ( ph -> ( C |`t W ) e. ( TopOn ` W ) )
39 toponss 
 |-  ( ( ( C |`t W ) e. ( TopOn ` W ) /\ x e. ( C |`t W ) ) -> x C_ W )
40 38 39 sylan 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> x C_ W )
41 f1imacnv 
 |-  ( ( ( F |` W ) : W -1-1-> A /\ x C_ W ) -> ( `' ( F |` W ) " ( ( F |` W ) " x ) ) = x )
42 29 40 41 syl2anc 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( `' ( F |` W ) " ( ( F |` W ) " x ) ) = x )
43 42 imaeq2d 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( `' ( H |` M ) " ( `' ( F |` W ) " ( ( F |` W ) " x ) ) ) = ( `' ( H |` M ) " x ) )
44 imaco 
 |-  ( ( `' ( H |` M ) o. `' ( F |` W ) ) " ( ( F |` W ) " x ) ) = ( `' ( H |` M ) " ( `' ( F |` W ) " ( ( F |` W ) " x ) ) )
45 cnvco 
 |-  `' ( ( F |` W ) o. ( H |` M ) ) = ( `' ( H |` M ) o. `' ( F |` W ) )
46 cores 
 |-  ( ran ( H |` M ) C_ W -> ( ( F |` W ) o. ( H |` M ) ) = ( F o. ( H |` M ) ) )
47 21 46 syl 
 |-  ( ph -> ( ( F |` W ) o. ( H |` M ) ) = ( F o. ( H |` M ) ) )
48 resco 
 |-  ( ( F o. H ) |` M ) = ( F o. ( H |` M ) )
49 47 48 eqtr4di 
 |-  ( ph -> ( ( F |` W ) o. ( H |` M ) ) = ( ( F o. H ) |` M ) )
50 49 adantr 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( ( F |` W ) o. ( H |` M ) ) = ( ( F o. H ) |` M ) )
51 50 cnveqd 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> `' ( ( F |` W ) o. ( H |` M ) ) = `' ( ( F o. H ) |` M ) )
52 45 51 eqtr3id 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( `' ( H |` M ) o. `' ( F |` W ) ) = `' ( ( F o. H ) |` M ) )
53 52 imaeq1d 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( ( `' ( H |` M ) o. `' ( F |` W ) ) " ( ( F |` W ) " x ) ) = ( `' ( ( F o. H ) |` M ) " ( ( F |` W ) " x ) ) )
54 44 53 eqtr3id 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( `' ( H |` M ) " ( `' ( F |` W ) " ( ( F |` W ) " x ) ) ) = ( `' ( ( F o. H ) |` M ) " ( ( F |` W ) " x ) ) )
55 43 54 eqtr3d 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( `' ( H |` M ) " x ) = ( `' ( ( F o. H ) |` M ) " ( ( F |` W ) " x ) ) )
56 2 cnrest 
 |-  ( ( ( F o. H ) e. ( K Cn J ) /\ M C_ Y ) -> ( ( F o. H ) |` M ) e. ( ( K |`t M ) Cn J ) )
57 6 11 56 syl2anc 
 |-  ( ph -> ( ( F o. H ) |` M ) e. ( ( K |`t M ) Cn J ) )
58 57 adantr 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( ( F o. H ) |` M ) e. ( ( K |`t M ) Cn J ) )
59 resima2 
 |-  ( x C_ W -> ( ( F |` W ) " x ) = ( F " x ) )
60 40 59 syl 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( ( F |` W ) " x ) = ( F " x ) )
61 4 adantr 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> F e. ( C CovMap J ) )
62 restopn2 
 |-  ( ( C e. Top /\ W e. C ) -> ( x e. ( C |`t W ) <-> ( x e. C /\ x C_ W ) ) )
63 14 34 62 syl2anc 
 |-  ( ph -> ( x e. ( C |`t W ) <-> ( x e. C /\ x C_ W ) ) )
64 63 simprbda 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> x e. C )
65 cvmopn 
 |-  ( ( F e. ( C CovMap J ) /\ x e. C ) -> ( F " x ) e. J )
66 61 64 65 syl2anc 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( F " x ) e. J )
67 60 66 eqeltrd 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( ( F |` W ) " x ) e. J )
68 cnima 
 |-  ( ( ( ( F o. H ) |` M ) e. ( ( K |`t M ) Cn J ) /\ ( ( F |` W ) " x ) e. J ) -> ( `' ( ( F o. H ) |` M ) " ( ( F |` W ) " x ) ) e. ( K |`t M ) )
69 58 67 68 syl2anc 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( `' ( ( F o. H ) |` M ) " ( ( F |` W ) " x ) ) e. ( K |`t M ) )
70 55 69 eqeltrd 
 |-  ( ( ph /\ x e. ( C |`t W ) ) -> ( `' ( H |` M ) " x ) e. ( K |`t M ) )
71 70 ralrimiva 
 |-  ( ph -> A. x e. ( C |`t W ) ( `' ( H |` M ) " x ) e. ( K |`t M ) )
72 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
73 7 72 sylib 
 |-  ( ph -> K e. ( TopOn ` Y ) )
74 resttopon 
 |-  ( ( K e. ( TopOn ` Y ) /\ M C_ Y ) -> ( K |`t M ) e. ( TopOn ` M ) )
75 73 11 74 syl2anc 
 |-  ( ph -> ( K |`t M ) e. ( TopOn ` M ) )
76 iscn 
 |-  ( ( ( K |`t M ) e. ( TopOn ` M ) /\ ( C |`t W ) e. ( TopOn ` W ) ) -> ( ( H |` M ) e. ( ( K |`t M ) Cn ( C |`t W ) ) <-> ( ( H |` M ) : M --> W /\ A. x e. ( C |`t W ) ( `' ( H |` M ) " x ) e. ( K |`t M ) ) ) )
77 75 38 76 syl2anc 
 |-  ( ph -> ( ( H |` M ) e. ( ( K |`t M ) Cn ( C |`t W ) ) <-> ( ( H |` M ) : M --> W /\ A. x e. ( C |`t W ) ( `' ( H |` M ) " x ) e. ( K |`t M ) ) ) )
78 23 71 77 mpbir2and 
 |-  ( ph -> ( H |` M ) e. ( ( K |`t M ) Cn ( C |`t W ) ) )
79 16 78 sseldd 
 |-  ( ph -> ( H |` M ) e. ( ( K |`t M ) Cn C ) )