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

Definition df-cvm 31212
 Description: Define the class of covering maps on two topological spaces. A function 𝑓:𝑐⟶𝑗 is a covering map if it is continuous and for every point 𝑥 in the target space there is a neighborhood 𝑘 of 𝑥 and a decomposition 𝑠 of the preimage of 𝑘 as a disjoint union such that 𝑓 is a homeomorphism of each set 𝑢 ∈ 𝑠 onto 𝑘. (Contributed by Mario Carneiro, 13-Feb-2015.)
Assertion
Ref Expression
df-cvm CovMap = (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))})
Distinct variable group:   𝑗,𝑐,𝑓,𝑥,𝑘,𝑠,𝑢,𝑣

Detailed syntax breakdown of Definition df-cvm
StepHypRef Expression
1 ccvm 31211 . 2 class CovMap
2 vc . . 3 setvar 𝑐
3 vj . . 3 setvar 𝑗
4 ctop 20679 . . 3 class Top
5 vx . . . . . . . 8 setvar 𝑥
6 vk . . . . . . . 8 setvar 𝑘
75, 6wel 1989 . . . . . . 7 wff 𝑥𝑘
8 vs . . . . . . . . . . . 12 setvar 𝑠
98cv 1480 . . . . . . . . . . 11 class 𝑠
109cuni 4427 . . . . . . . . . 10 class 𝑠
11 vf . . . . . . . . . . . . 13 setvar 𝑓
1211cv 1480 . . . . . . . . . . . 12 class 𝑓
1312ccnv 5103 . . . . . . . . . . 11 class 𝑓
146cv 1480 . . . . . . . . . . 11 class 𝑘
1513, 14cima 5107 . . . . . . . . . 10 class (𝑓𝑘)
1610, 15wceq 1481 . . . . . . . . 9 wff 𝑠 = (𝑓𝑘)
17 vu . . . . . . . . . . . . . . 15 setvar 𝑢
1817cv 1480 . . . . . . . . . . . . . 14 class 𝑢
19 vv . . . . . . . . . . . . . . 15 setvar 𝑣
2019cv 1480 . . . . . . . . . . . . . 14 class 𝑣
2118, 20cin 3566 . . . . . . . . . . . . 13 class (𝑢𝑣)
22 c0 3907 . . . . . . . . . . . . 13 class
2321, 22wceq 1481 . . . . . . . . . . . 12 wff (𝑢𝑣) = ∅
2418csn 4168 . . . . . . . . . . . . 13 class {𝑢}
259, 24cdif 3564 . . . . . . . . . . . 12 class (𝑠 ∖ {𝑢})
2623, 19, 25wral 2909 . . . . . . . . . . 11 wff 𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅
2712, 18cres 5106 . . . . . . . . . . . 12 class (𝑓𝑢)
282cv 1480 . . . . . . . . . . . . . 14 class 𝑐
29 crest 16062 . . . . . . . . . . . . . 14 class t
3028, 18, 29co 6635 . . . . . . . . . . . . 13 class (𝑐t 𝑢)
313cv 1480 . . . . . . . . . . . . . 14 class 𝑗
3231, 14, 29co 6635 . . . . . . . . . . . . 13 class (𝑗t 𝑘)
33 chmeo 21537 . . . . . . . . . . . . 13 class Homeo
3430, 32, 33co 6635 . . . . . . . . . . . 12 class ((𝑐t 𝑢)Homeo(𝑗t 𝑘))
3527, 34wcel 1988 . . . . . . . . . . 11 wff (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))
3626, 35wa 384 . . . . . . . . . 10 wff (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))
3736, 17, 9wral 2909 . . . . . . . . 9 wff 𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))
3816, 37wa 384 . . . . . . . 8 wff ( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))))
3928cpw 4149 . . . . . . . . 9 class 𝒫 𝑐
4022csn 4168 . . . . . . . . 9 class {∅}
4139, 40cdif 3564 . . . . . . . 8 class (𝒫 𝑐 ∖ {∅})
4238, 8, 41wrex 2910 . . . . . . 7 wff 𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))))
437, 42wa 384 . . . . . 6 wff (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
4443, 6, 31wrex 2910 . . . . 5 wff 𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
4531cuni 4427 . . . . 5 class 𝑗
4644, 5, 45wral 2909 . . . 4 wff 𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
47 ccn 21009 . . . . 5 class Cn
4828, 31, 47co 6635 . . . 4 class (𝑐 Cn 𝑗)
4946, 11, 48crab 2913 . . 3 class {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))}
502, 3, 4, 4, 49cmpt2 6637 . 2 class (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))})
511, 50wceq 1481 1 wff CovMap = (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))})
 Colors of variables: wff setvar class This definition is referenced by:  fncvm  31213  iscvm  31215
 Copyright terms: Public domain W3C validator