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

Definition df-cvm 23787
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 23786 . 2  class CovMap
2 vc . . 3  set  c
3 vj . . 3  set  j
4 ctop 16631 . . 3  class  Top
5 vx . . . . . . . 8  set  x
6 vk . . . . . . . 8  set  k
75, 6wel 1685 . . . . . . 7  wff  x  e.  k
8 vs . . . . . . . . . . . 12  set  s
98cv 1622 . . . . . . . . . . 11  class  s
109cuni 3827 . . . . . . . . . 10  class  U. s
11 vf . . . . . . . . . . . . 13  set  f
1211cv 1622 . . . . . . . . . . . 12  class  f
1312ccnv 4688 . . . . . . . . . . 11  class  `' f
146cv 1622 . . . . . . . . . . 11  class  k
1513, 14cima 4692 . . . . . . . . . 10  class  ( `' f " k )
1610, 15wceq 1623 . . . . . . . . 9  wff  U. s  =  ( `' f
" k )
17 vu . . . . . . . . . . . . . . 15  set  u
1817cv 1622 . . . . . . . . . . . . . 14  class  u
19 vv . . . . . . . . . . . . . . 15  set  v
2019cv 1622 . . . . . . . . . . . . . 14  class  v
2118, 20cin 3151 . . . . . . . . . . . . 13  class  ( u  i^i  v )
22 c0 3455 . . . . . . . . . . . . 13  class  (/)
2321, 22wceq 1623 . . . . . . . . . . . 12  wff  ( u  i^i  v )  =  (/)
2418csn 3640 . . . . . . . . . . . . 13  class  { u }
259, 24cdif 3149 . . . . . . . . . . . 12  class  ( s 
\  { u }
)
2623, 19, 25wral 2543 . . . . . . . . . . 11  wff  A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)
2712, 18cres 4691 . . . . . . . . . . . 12  class  ( f  |`  u )
282cv 1622 . . . . . . . . . . . . . 14  class  c
29 crest 13325 . . . . . . . . . . . . . 14  classt
3028, 18, 29co 5858 . . . . . . . . . . . . 13  class  ( ct  u )
313cv 1622 . . . . . . . . . . . . . 14  class  j
3231, 14, 29co 5858 . . . . . . . . . . . . 13  class  ( jt  k )
33 chmeo 17444 . . . . . . . . . . . . 13  class  Homeo
3430, 32, 33co 5858 . . . . . . . . . . . 12  class  ( ( ct  u )  Homeo  ( jt  k ) )
3527, 34wcel 1684 . . . . . . . . . . 11  wff  ( f  |`  u )  e.  ( ( ct  u )  Homeo  ( jt  k ) )
3626, 35wa 358 . . . . . . . . . 10  wff  ( A. v  e.  ( s  \  { u } ) ( u  i^i  v
)  =  (/)  /\  (
f  |`  u )  e.  ( ( ct  u ) 
Homeo  ( jt  k ) ) )
3736, 17, 9wral 2543 . . . . . . . . 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 358 . . . . . . . 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 3625 . . . . . . . . 9  class  ~P c
4022csn 3640 . . . . . . . . 9  class  { (/) }
4139, 40cdif 3149 . . . . . . . 8  class  ( ~P c  \  { (/) } )
4238, 8, 41wrex 2544 . . . . . . 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 358 . . . . . 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 2544 . . . . 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 3827 . . . . 5  class  U. j
4644, 5, 45wral 2543 . . . 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 16954 . . . . 5  class  Cn
4828, 31, 47co 5858 . . . 4  class  ( c  Cn  j )
4946, 11, 48crab 2547 . . 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 5860 . 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 1623 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 set class
This definition is referenced by:  fncvm  23788  iscvm  23790
  Copyright terms: Public domain W3C validator