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 Top , j Top f c Cn j | x j k j x k s 𝒫 c s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccvm class CovMap
1 vc setvar c
2 ctop class Top
3 vj setvar j
4 vf setvar f
5 1 cv setvar c
6 ccn class Cn
7 3 cv setvar j
8 5 7 6 co class c Cn j
9 vx setvar x
10 7 cuni class j
11 vk setvar k
12 9 cv setvar x
13 11 cv setvar k
14 12 13 wcel wff x k
15 vs setvar s
16 5 cpw class 𝒫 c
17 c0 class
18 17 csn class
19 16 18 cdif class 𝒫 c
20 15 cv setvar s
21 20 cuni class s
22 4 cv setvar f
23 22 ccnv class f -1
24 23 13 cima class f -1 k
25 21 24 wceq wff s = f -1 k
26 vu setvar u
27 vv setvar v
28 26 cv setvar u
29 28 csn class u
30 20 29 cdif class s u
31 27 cv setvar v
32 28 31 cin class u v
33 32 17 wceq wff u v =
34 33 27 30 wral wff v s u u v =
35 22 28 cres class f u
36 crest class 𝑡
37 5 28 36 co class c 𝑡 u
38 chmeo class Homeo
39 7 13 36 co class j 𝑡 k
40 37 39 38 co class c 𝑡 u Homeo j 𝑡 k
41 35 40 wcel wff f u c 𝑡 u Homeo j 𝑡 k
42 34 41 wa wff v s u u v = f u c 𝑡 u Homeo j 𝑡 k
43 42 26 20 wral wff u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k
44 25 43 wa wff s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k
45 44 15 19 wrex wff s 𝒫 c s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k
46 14 45 wa wff x k s 𝒫 c s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k
47 46 11 7 wrex wff k j x k s 𝒫 c s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k
48 47 9 10 wral wff x j k j x k s 𝒫 c s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k
49 48 4 8 crab class f c Cn j | x j k j x k s 𝒫 c s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k
50 1 3 2 2 49 cmpo class c Top , j Top f c Cn j | x j k j x k s 𝒫 c s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k
51 0 50 wceq wff CovMap = c Top , j Top f c Cn j | x j k j x k s 𝒫 c s = f -1 k u s v s u u v = f u c 𝑡 u Homeo j 𝑡 k