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 32789
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 32788 . 2 class CovMap
2 vc . . 3 setvar 𝑐
3 vj . . 3 setvar 𝑗
4 ctop 21644 . . 3 class Top
5 vx . . . . . . . 8 setvar 𝑥
6 vk . . . . . . . 8 setvar 𝑘
75, 6wel 2115 . . . . . . 7 wff 𝑥𝑘
8 vs . . . . . . . . . . . 12 setvar 𝑠
98cv 1541 . . . . . . . . . . 11 class 𝑠
109cuni 4796 . . . . . . . . . 10 class 𝑠
11 vf . . . . . . . . . . . . 13 setvar 𝑓
1211cv 1541 . . . . . . . . . . . 12 class 𝑓
1312ccnv 5524 . . . . . . . . . . 11 class 𝑓
146cv 1541 . . . . . . . . . . 11 class 𝑘
1513, 14cima 5528 . . . . . . . . . 10 class (𝑓𝑘)
1610, 15wceq 1542 . . . . . . . . 9 wff 𝑠 = (𝑓𝑘)
17 vu . . . . . . . . . . . . . . 15 setvar 𝑢
1817cv 1541 . . . . . . . . . . . . . 14 class 𝑢
19 vv . . . . . . . . . . . . . . 15 setvar 𝑣
2019cv 1541 . . . . . . . . . . . . . 14 class 𝑣
2118, 20cin 3842 . . . . . . . . . . . . 13 class (𝑢𝑣)
22 c0 4211 . . . . . . . . . . . . 13 class
2321, 22wceq 1542 . . . . . . . . . . . 12 wff (𝑢𝑣) = ∅
2418csn 4516 . . . . . . . . . . . . 13 class {𝑢}
259, 24cdif 3840 . . . . . . . . . . . 12 class (𝑠 ∖ {𝑢})
2623, 19, 25wral 3053 . . . . . . . . . . 11 wff 𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅
2712, 18cres 5527 . . . . . . . . . . . 12 class (𝑓𝑢)
282cv 1541 . . . . . . . . . . . . . 14 class 𝑐
29 crest 16797 . . . . . . . . . . . . . 14 class t
3028, 18, 29co 7170 . . . . . . . . . . . . 13 class (𝑐t 𝑢)
313cv 1541 . . . . . . . . . . . . . 14 class 𝑗
3231, 14, 29co 7170 . . . . . . . . . . . . 13 class (𝑗t 𝑘)
33 chmeo 22504 . . . . . . . . . . . . 13 class Homeo
3430, 32, 33co 7170 . . . . . . . . . . . 12 class ((𝑐t 𝑢)Homeo(𝑗t 𝑘))
3527, 34wcel 2114 . . . . . . . . . . 11 wff (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))
3626, 35wa 399 . . . . . . . . . 10 wff (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))
3736, 17, 9wral 3053 . . . . . . . . 9 wff 𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))
3816, 37wa 399 . . . . . . . 8 wff ( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))))
3928cpw 4488 . . . . . . . . 9 class 𝒫 𝑐
4022csn 4516 . . . . . . . . 9 class {∅}
4139, 40cdif 3840 . . . . . . . 8 class (𝒫 𝑐 ∖ {∅})
4238, 8, 41wrex 3054 . . . . . . 7 wff 𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘))))
437, 42wa 399 . . . . . 6 wff (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
4443, 6, 31wrex 3054 . . . . 5 wff 𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
4531cuni 4796 . . . . 5 class 𝑗
4644, 5, 45wral 3053 . . . 4 wff 𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))
47 ccn 21975 . . . . 5 class Cn
4828, 31, 47co 7170 . . . 4 class (𝑐 Cn 𝑗)
4946, 11, 48crab 3057 . . 3 class {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))}
502, 3, 4, 4, 49cmpo 7172 . 2 class (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))})
511, 50wceq 1542 1 wff CovMap = (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 𝑗𝑘𝑗 (𝑥𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})( 𝑠 = (𝑓𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝑓𝑢) ∈ ((𝑐t 𝑢)Homeo(𝑗t 𝑘)))))})
Colors of variables: wff setvar class
This definition is referenced by:  fncvm  32790  iscvm  32792
  Copyright terms: Public domain W3C validator