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 = ( 𝑐 ∈ Top , 𝑗 ∈ Top ↦ { 𝑓 ∈ ( 𝑐 Cn 𝑗 ) ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccvm	⊢ CovMap
1		vc	⊢ 𝑐
2		ctop	⊢ Top
3		vj	⊢ 𝑗
4		vf	⊢ 𝑓
5	1	cv	⊢ 𝑐
6		ccn	⊢ Cn
7	3	cv	⊢ 𝑗
8	5 7 6	co	⊢ ( 𝑐 Cn 𝑗 )
9		vx	⊢ 𝑥
10	7	cuni	⊢ ∪ 𝑗
11		vk	⊢ 𝑘
12	9	cv	⊢ 𝑥
13	11	cv	⊢ 𝑘
14	12 13	wcel	⊢ 𝑥 ∈ 𝑘
15		vs	⊢ 𝑠
16	5	cpw	⊢ 𝒫 𝑐
17		c0	⊢ ∅
18	17	csn	⊢ { ∅ }
19	16 18	cdif	⊢ ( 𝒫 𝑐 ∖ { ∅ } )
20	15	cv	⊢ 𝑠
21	20	cuni	⊢ ∪ 𝑠
22	4	cv	⊢ 𝑓
23	22	ccnv	⊢ ◡ 𝑓
24	23 13	cima	⊢ ( ◡ 𝑓 “ 𝑘 )
25	21 24	wceq	⊢ ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 )
26		vu	⊢ 𝑢
27		vv	⊢ 𝑣
28	26	cv	⊢ 𝑢
29	28	csn	⊢ { 𝑢 }
30	20 29	cdif	⊢ ( 𝑠 ∖ { 𝑢 } )
31	27	cv	⊢ 𝑣
32	28 31	cin	⊢ ( 𝑢 ∩ 𝑣 )
33	32 17	wceq	⊢ ( 𝑢 ∩ 𝑣 ) = ∅
34	33 27 30	wral	⊢ ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅
35	22 28	cres	⊢ ( 𝑓 ↾ 𝑢 )
36		crest	⊢ ↾t
37	5 28 36	co	⊢ ( 𝑐 ↾t 𝑢 )
38		chmeo	⊢ Homeo
39	7 13 36	co	⊢ ( 𝑗 ↾t 𝑘 )
40	37 39 38	co	⊢ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) )
41	35 40	wcel	⊢ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) )
42	34 41	wa	⊢ ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) )
43	42 26 20	wral	⊢ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) )
44	25 43	wa	⊢ ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) )
45	44 15 19	wrex	⊢ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) )
46	14 45	wa	⊢ ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) )
47	46 11 7	wrex	⊢ ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) )
48	47 9 10	wral	⊢ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) )
49	48 4 8	crab	⊢ { 𝑓 ∈ ( 𝑐 Cn 𝑗 ) ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) }
50	1 3 2 2 49	cmpo	⊢ ( 𝑐 ∈ Top , 𝑗 ∈ Top ↦ { 𝑓 ∈ ( 𝑐 Cn 𝑗 ) ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) } )
51	0 50	wceq	⊢ CovMap = ( 𝑐 ∈ Top , 𝑗 ∈ Top ↦ { 𝑓 ∈ ( 𝑐 Cn 𝑗 ) ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) } )