Metamath Proof Explorer

Definition df-cvm

Description: Define the class of covering maps on two topological spaces. A function f : c --> j is a covering map if it is continuous and for every point x in the target space there is a neighborhood k of x and a decomposition s of the preimage of k as a disjoint union such that f is a homeomorphism of each set u e. s onto k . (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Assertion df-cvm 
|- CovMap = ( c e. Top , j e. Top |-> { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. 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 ) ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccvm 
 |-  CovMap
1 vc 
 |-  c
2 ctop 
 |-  Top
3 vj 
 |-  j
4 vf 
 |-  f
5 1 cv 
 |-  c
6 ccn 
 |-  Cn
7 3 cv 
 |-  j
8 5 7 6 co 
 |-  ( c Cn j )
9 vx 
 |-  x
10 7 cuni 
 |-  U. j
11 vk 
 |-  k
12 9 cv 
 |-  x
13 11 cv 
 |-  k
14 12 13 wcel 
 |-  x e. k
15 vs 
 |-  s
16 5 cpw 
 |-  ~P c
17 c0 
 |-  (/)
18 17 csn 
 |-  { (/) }
19 16 18 cdif 
 |-  ( ~P c \ { (/) } )
20 15 cv 
 |-  s
21 20 cuni 
 |-  U. s
22 4 cv 
 |-  f
23 22 ccnv 
 |-  `' f
24 23 13 cima 
 |-  ( `' f " k )
25 21 24 wceq 
 |-  U. s = ( `' f " k )
26 vu 
 |-  u
27 vv 
 |-  v
28 26 cv 
 |-  u
29 28 csn 
 |-  { u }
30 20 29 cdif 
 |-  ( s \ { u } )
31 27 cv 
 |-  v
32 28 31 cin 
 |-  ( u i^i v )
33 32 17 wceq 
 |-  ( u i^i v ) = (/)
34 33 27 30 wral 
 |-  A. v e. ( s \ { u } ) ( u i^i v ) = (/)
35 22 28 cres 
 |-  ( f |` u )
36 crest 
 |-  |`t
37 5 28 36 co 
 |-  ( c |`t u )
38 chmeo 
 |-  Homeo
39 7 13 36 co 
 |-  ( j |`t k )
40 37 39 38 co 
 |-  ( ( c |`t u ) Homeo ( j |`t k ) )
41 35 40 wcel 
 |-  ( f |` u ) e. ( ( c |`t u ) Homeo ( j |`t k ) )
42 34 41 wa 
 |-  ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c |`t u ) Homeo ( j |`t k ) ) )
43 42 26 20 wral 
 |-  A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c |`t u ) Homeo ( j |`t k ) ) )
44 25 43 wa 
 |-  ( 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 ) ) ) )
45 44 15 19 wrex 
 |-  E. 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 ) ) ) )
46 14 45 wa 
 |-  ( x e. k /\ E. 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 ) ) ) ) )
47 46 11 7 wrex 
 |-  E. k e. j ( x e. k /\ E. 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 ) ) ) ) )
48 47 9 10 wral 
 |-  A. x e. U. j E. k e. j ( x e. k /\ E. 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 ) ) ) ) )
49 48 4 8 crab 
 |-  { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. 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 ) ) ) ) ) }
50 1 3 2 2 49 cmpo 
 |-  ( c e. Top , j e. Top |-> { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. 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 ) ) ) ) ) } )
51 0 50 wceq 
 |-  CovMap = ( c e. Top , j e. Top |-> { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. 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 ) ) ) ) ) } )