Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cvm Structured version   Unicode version

Definition df-cvm 27160
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.)
Assertion
Ref Expression
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.  ( ( ct  u )
Homeo ( jt  k ) ) ) ) ) } )
Distinct variable group:    j, c, f, x, k, s, u, v

Detailed syntax breakdown of Definition df-cvm
StepHypRef Expression
1 ccvm 27159 . 2  class CovMap
2 vc . . 3  setvar  c
3 vj . . 3  setvar  j
4 ctop 18513 . . 3  class  Top
5 vx . . . . . . . 8  setvar  x
6 vk . . . . . . . 8  setvar  k
75, 6wel 1757 . . . . . . 7  wff  x  e.  k
8 vs . . . . . . . . . . . 12  setvar  s
98cv 1368 . . . . . . . . . . 11  class  s
109cuni 4106 . . . . . . . . . 10  class  U. s
11 vf . . . . . . . . . . . . 13  setvar  f
1211cv 1368 . . . . . . . . . . . 12  class  f
1312ccnv 4854 . . . . . . . . . . 11  class  `' f
146cv 1368 . . . . . . . . . . 11  class  k
1513, 14cima 4858 . . . . . . . . . 10  class  ( `' f " k )
1610, 15wceq 1369 . . . . . . . . 9  wff  U. s  =  ( `' f
" k )
17 vu . . . . . . . . . . . . . . 15  setvar  u
1817cv 1368 . . . . . . . . . . . . . 14  class  u
19 vv . . . . . . . . . . . . . . 15  setvar  v
2019cv 1368 . . . . . . . . . . . . . 14  class  v
2118, 20cin 3342 . . . . . . . . . . . . 13  class  ( u  i^i  v )
22 c0 3652 . . . . . . . . . . . . 13  class  (/)
2321, 22wceq 1369 . . . . . . . . . . . 12  wff  ( u  i^i  v )  =  (/)
2418csn 3892 . . . . . . . . . . . . 13  class  { u }
259, 24cdif 3340 . . . . . . . . . . . 12  class  ( s 
\  { u }
)
2623, 19, 25wral 2730 . . . . . . . . . . 11  wff  A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)
2712, 18cres 4857 . . . . . . . . . . . 12  class  ( f  |`  u )
282cv 1368 . . . . . . . . . . . . . 14  class  c
29 crest 14374 . . . . . . . . . . . . . 14  classt
3028, 18, 29co 6106 . . . . . . . . . . . . 13  class  ( ct  u )
313cv 1368 . . . . . . . . . . . . . 14  class  j
3231, 14, 29co 6106 . . . . . . . . . . . . 13  class  ( jt  k )
33 chmeo 19341 . . . . . . . . . . . . 13  class  Homeo
3430, 32, 33co 6106 . . . . . . . . . . . 12  class  ( ( ct  u ) Homeo ( jt  k ) )
3527, 34wcel 1756 . . . . . . . . . . 11  wff  ( f  |`  u )  e.  ( ( ct  u ) Homeo ( jt  k ) )
3626, 35wa 369 . . . . . . . . . 10  wff  ( A. v  e.  ( s  \  { u } ) ( u  i^i  v
)  =  (/)  /\  (
f  |`  u )  e.  ( ( ct  u )
Homeo ( jt  k ) ) )
3736, 17, 9wral 2730 . . . . . . . . 9  wff  A. u  e.  s  ( A. v  e.  ( s  \  { u } ) ( u  i^i  v
)  =  (/)  /\  (
f  |`  u )  e.  ( ( ct  u )
Homeo ( jt  k ) ) )
3816, 37wa 369 . . . . . . . 8  wff  ( U. s  =  ( `' f " k )  /\  A. u  e.  s  ( A. v  e.  ( s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( f  |`  u )  e.  ( ( ct  u ) Homeo ( jt  k ) ) ) )
3928cpw 3875 . . . . . . . . 9  class  ~P c
4022csn 3892 . . . . . . . . 9  class  { (/) }
4139, 40cdif 3340 . . . . . . . 8  class  ( ~P c  \  { (/) } )
4238, 8, 41wrex 2731 . . . . . . 7  wff  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.  ( ( ct  u )
Homeo ( jt  k ) ) ) )
437, 42wa 369 . . . . . 6  wff  ( 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.  ( ( ct  u ) Homeo ( jt  k ) ) ) ) )
4443, 6, 31wrex 2731 . . . . 5  wff  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.  ( ( ct  u )
Homeo ( jt  k ) ) ) ) )
4531cuni 4106 . . . . 5  class  U. j
4644, 5, 45wral 2730 . . . 4  wff  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.  ( ( ct  u )
Homeo ( jt  k ) ) ) ) )
47 ccn 18843 . . . . 5  class  Cn
4828, 31, 47co 6106 . . . 4  class  ( c  Cn  j )
4946, 11, 48crab 2734 . . 3  class  { 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.  ( ( ct  u )
Homeo ( jt  k ) ) ) ) ) }
502, 3, 4, 4, 49cmpt2 6108 . 2  class  ( 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.  ( ( ct  u )
Homeo ( jt  k ) ) ) ) ) } )
511, 50wceq 1369 1  wff 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.  ( ( ct  u )
Homeo ( jt  k ) ) ) ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  fncvm  27161  iscvm  27163
  Copyright terms: Public domain W3C validator