Users' Mathboxes 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 30294
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 30293 . 2 class CovMap
2 vc . . 3 setvar 𝑐
3 vj . . 3 setvar 𝑗
4 ctop 20455 . . 3 class Top
5 vx . . . . . . . 8 setvar 𝑥
6 vk . . . . . . . 8 setvar 𝑘
75, 6wel 1976 . . . . . . 7 wff 𝑥𝑘
8 vs . . . . . . . . . . . 12 setvar 𝑠
98cv 1473 . . . . . . . . . . 11 class 𝑠
109cuni 4362 . . . . . . . . . 10 class 𝑠
11 vf . . . . . . . . . . . . 13 setvar 𝑓
1211cv 1473 . . . . . . . . . . . 12 class 𝑓
1312ccnv 5023 . . . . . . . . . . 11 class 𝑓
146cv 1473 . . . . . . . . . . 11 class 𝑘
1513, 14cima 5027 . . . . . . . . . 10 class (𝑓𝑘)
1610, 15wceq 1474 . . . . . . . . 9 wff 𝑠 = (𝑓𝑘)
17 vu . . . . . . . . . . . . . . 15 setvar 𝑢
1817cv 1473 . . . . . . . . . . . . . 14 class 𝑢
19 vv . . . . . . . . . . . . . . 15 setvar 𝑣
2019cv 1473 . . . . . . . . . . . . . 14 class 𝑣
2118, 20cin 3534 . . . . . . . . . . . . 13 class (𝑢𝑣)
22 c0 3869 . . . . . . . . . . . . 13 class
2321, 22wceq 1474 . . . . . . . . . . . 12 wff (𝑢𝑣) = ∅
2418csn 4120 . . . . . . . . . . . . 13 class {𝑢}
259, 24cdif 3532 . . . . . . . . . . . 12 class (𝑠 ∖ {𝑢})
2623, 19, 25wral 2891 . . . . . . . . . . 11 wff 𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅
2712, 18cres 5026 . . . . . . . . . . . 12 class (𝑓𝑢)
282cv 1473 . . . . . . . . . . . . . 14 class 𝑐
29 crest 15846 . . . . . . . . . . . . . 14 class t
3028, 18, 29co 6523 . . . . . . . . . . . . 13 class (𝑐t 𝑢)
313cv 1473 . . . . . . . . . . . . . 14 class 𝑗
3231, 14, 29co 6523 . . . . . . . . . . . . 13 class (𝑗t 𝑘)
33 chmeo 21304 . . . . . . . . . . . . 13 class Homeo
3430, 32, 33co 6523 . . . . . . . . . . . 12 class ((𝑐t 𝑢)Homeo(𝑗t 𝑘))
3527, 34wcel 1975 . . . . . . . . . . 11 wff (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))
3626, 35wa 382 . . . . . . . . . 10 wff (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))
3736, 17, 9wral 2891 . . . . . . . . 9 wff 𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))
3816, 37wa 382 . . . . . . . 8 wff ( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))))
3928cpw 4103 . . . . . . . . 9 class 𝒫 𝑐
4022csn 4120 . . . . . . . . 9 class {∅}
4139, 40cdif 3532 . . . . . . . 8 class (𝒫 𝑐 ∖ {∅})
4238, 8, 41wrex 2892 . . . . . . 7 wff 𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))))
437, 42wa 382 . . . . . 6 wff (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
4443, 6, 31wrex 2892 . . . . 5 wff 𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
4531cuni 4362 . . . . 5 class 𝑗
4644, 5, 45wral 2891 . . . 4 wff 𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
47 ccn 20776 . . . . 5 class Cn
4828, 31, 47co 6523 . . . 4 class (𝑐 Cn 𝑗)
4946, 11, 48crab 2895 . . 3 class {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))}
502, 3, 4, 4, 49cmpt2 6525 . 2 class (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))})
511, 50wceq 1474 1 wff CovMap = (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))})
Colors of variables: wff setvar class
This definition is referenced by:  fncvm  30295  iscvm  30297
  Copyright terms: Public domain W3C validator