Definition df-cvm 35261

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

Step	Hyp	Ref	Expression
1		ccvm 35260	. 2 class CovMap
2		vc	. . 3 setvar 𝑐
3		vj	. . 3 setvar 𝑗
4		ctop 22899	. . 3 class Top
5		vx	. . . . . . . 8 setvar 𝑥
6		vk	. . . . . . . 8 setvar 𝑘
7	5, 6	wel 2109	. . . . . . 7 wff 𝑥 ∈ 𝑘
8		vs	. . . . . . . . . . . 12 setvar 𝑠
9	8	cv 1539	. . . . . . . . . . 11 class 𝑠
10	9	cuni 4907	. . . . . . . . . 10 class ∪ 𝑠
11		vf	. . . . . . . . . . . . 13 setvar 𝑓
12	11	cv 1539	. . . . . . . . . . . 12 class 𝑓
13	12	ccnv 5684	. . . . . . . . . . 11 class ◡𝑓
14	6	cv 1539	. . . . . . . . . . 11 class 𝑘
15	13, 14	cima 5688	. . . . . . . . . 10 class (◡𝑓 “ 𝑘)
16	10, 15	wceq 1540	. . . . . . . . 9 wff ∪ 𝑠 = (◡𝑓 “ 𝑘)
17		vu	. . . . . . . . . . . . . . 15 setvar 𝑢
18	17	cv 1539	. . . . . . . . . . . . . 14 class 𝑢
19		vv	. . . . . . . . . . . . . . 15 setvar 𝑣
20	19	cv 1539	. . . . . . . . . . . . . 14 class 𝑣
21	18, 20	cin 3950	. . . . . . . . . . . . 13 class (𝑢 ∩ 𝑣)
22		c0 4333	. . . . . . . . . . . . 13 class ∅
23	21, 22	wceq 1540	. . . . . . . . . . . 12 wff (𝑢 ∩ 𝑣) = ∅
24	18	csn 4626	. . . . . . . . . . . . 13 class {𝑢}
25	9, 24	cdif 3948	. . . . . . . . . . . 12 class (𝑠 ∖ {𝑢})
26	23, 19, 25	wral 3061	. . . . . . . . . . 11 wff ∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅
27	12, 18	cres 5687	. . . . . . . . . . . 12 class (𝑓 ↾ 𝑢)
28	2	cv 1539	. . . . . . . . . . . . . 14 class 𝑐
29		crest 17465	. . . . . . . . . . . . . 14 class ↾t
30	28, 18, 29	co 7431	. . . . . . . . . . . . 13 class (𝑐 ↾t 𝑢)
31	3	cv 1539	. . . . . . . . . . . . . 14 class 𝑗
32	31, 14, 29	co 7431	. . . . . . . . . . . . 13 class (𝑗 ↾t 𝑘)
33		chmeo 23761	. . . . . . . . . . . . 13 class Homeo
34	30, 32, 33	co 7431	. . . . . . . . . . . 12 class ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))
35	27, 34	wcel 2108	. . . . . . . . . . 11 wff (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))
36	26, 35	wa 395	. . . . . . . . . 10 wff (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))
37	36, 17, 9	wral 3061	. . . . . . . . 9 wff ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))
38	16, 37	wa 395	. . . . . . . 8 wff (∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))))
39	28	cpw 4600	. . . . . . . . 9 class 𝒫 𝑐
40	22	csn 4626	. . . . . . . . 9 class {∅}
41	39, 40	cdif 3948	. . . . . . . 8 class (𝒫 𝑐 ∖ {∅})
42	38, 8, 41	wrex 3070	. . . . . . 7 wff ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))))
43	7, 42	wa 395	. . . . . 6 wff (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))
44	43, 6, 31	wrex 3070	. . . . 5 wff ∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))
45	31	cuni 4907	. . . . 5 class ∪ 𝑗
46	44, 5, 45	wral 3061	. . . 4 wff ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))
47		ccn 23232	. . . . 5 class Cn
48	28, 31, 47	co 7431	. . . 4 class (𝑐 Cn 𝑗)
49	46, 11, 48	crab 3436	. . 3 class {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))}
50	2, 3, 4, 4, 49	cmpo 7433	. 2 class (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))})
51	1, 50	wceq 1540	1 wff CovMap = (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))})

This definition is referenced by:  fncvm  35262  iscvm  35264