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