Definition df-cvm 31238

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.)

Assertion

Ref	Expression
df-cvm	|- CovMap = ( c e. Top , j e. Top |-> { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. s e. ( ~P c \ { (/) } ) ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) ) ) } )

Distinct variable group:   j, c, f, x, k, s, u, v

Detailed syntax breakdown of Definition df-cvm

Step	Hyp	Ref	Expression
1		ccvm 31237	. 2 class CovMap
2		vc	. . 3 setvar c
3		vj	. . 3 setvar j
4		ctop 20698	. . 3 class Top
5		vx	. . . . . . . 8 setvar x
6		vk	. . . . . . . 8 setvar k
7	5, 6	wel 1991	. . . . . . 7 wff x e. k
8		vs	. . . . . . . . . . . 12 setvar s
9	8	cv 1482	. . . . . . . . . . 11 class s
10	9	cuni 4436	. . . . . . . . . 10 class U. s
11		vf	. . . . . . . . . . . . 13 setvar f
12	11	cv 1482	. . . . . . . . . . . 12 class f
13	12	ccnv 5113	. . . . . . . . . . 11 class `' f
14	6	cv 1482	. . . . . . . . . . 11 class k
15	13, 14	cima 5117	. . . . . . . . . 10 class ( `' f " k )
16	10, 15	wceq 1483	. . . . . . . . 9 wff U. s = ( `' f " k )
17		vu	. . . . . . . . . . . . . . 15 setvar u
18	17	cv 1482	. . . . . . . . . . . . . 14 class u
19		vv	. . . . . . . . . . . . . . 15 setvar v
20	19	cv 1482	. . . . . . . . . . . . . 14 class v
21	18, 20	cin 3573	. . . . . . . . . . . . 13 class ( u i^i v )
22		c0 3915	. . . . . . . . . . . . 13 class (/)
23	21, 22	wceq 1483	. . . . . . . . . . . 12 wff ( u i^i v ) = (/)
24	18	csn 4177	. . . . . . . . . . . . 13 class { u }
25	9, 24	cdif 3571	. . . . . . . . . . . 12 class ( s \ { u } )
26	23, 19, 25	wral 2912	. . . . . . . . . . 11 wff A. v e. ( s \ { u } ) ( u i^i v ) = (/)
27	12, 18	cres 5116	. . . . . . . . . . . 12 class ( f |` u )
28	2	cv 1482	. . . . . . . . . . . . . 14 class c
29		crest 16081	. . . . . . . . . . . . . 14 class ↾t
30	28, 18, 29	co 6650	. . . . . . . . . . . . 13 class ( c ↾t u )
31	3	cv 1482	. . . . . . . . . . . . . 14 class j
32	31, 14, 29	co 6650	. . . . . . . . . . . . 13 class ( j ↾t k )
33		chmeo 21556	. . . . . . . . . . . . 13 class Homeo
34	30, 32, 33	co 6650	. . . . . . . . . . . 12 class ( ( c ↾t u ) Homeo ( j ↾t k ) )
35	27, 34	wcel 1990	. . . . . . . . . . 11 wff ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) )
36	26, 35	wa 384	. . . . . . . . . 10 wff ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) )
37	36, 17, 9	wral 2912	. . . . . . . . 9 wff A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) )
38	16, 37	wa 384	. . . . . . . 8 wff ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) )
39	28	cpw 4158	. . . . . . . . 9 class ~P c
40	22	csn 4177	. . . . . . . . 9 class { (/) }
41	39, 40	cdif 3571	. . . . . . . 8 class ( ~P c \ { (/) } )
42	38, 8, 41	wrex 2913	. . . . . . 7 wff E. s e. ( ~P c \ { (/) } ) ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) )
43	7, 42	wa 384	. . . . . 6 wff ( x e. k /\ E. s e. ( ~P c \ { (/) } ) ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) ) )
44	43, 6, 31	wrex 2913	. . . . 5 wff E. k e. j ( x e. k /\ E. s e. ( ~P c \ { (/) } ) ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) ) )
45	31	cuni 4436	. . . . 5 class U. j
46	44, 5, 45	wral 2912	. . . 4 wff A. x e. U. j E. k e. j ( x e. k /\ E. s e. ( ~P c \ { (/) } ) ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) ) )
47		ccn 21028	. . . . 5 class Cn
48	28, 31, 47	co 6650	. . . 4 class ( c Cn j )
49	46, 11, 48	crab 2916	. . 3 class { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. s e. ( ~P c \ { (/) } ) ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) ) ) }
50	2, 3, 4, 4, 49	cmpt2 6652	. 2 class ( c e. Top , j e. Top |-> { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. s e. ( ~P c \ { (/) } ) ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) ) ) } )
51	1, 50	wceq 1483	1 wff CovMap = ( c e. Top , j e. Top |-> { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. s e. ( ~P c \ { (/) } ) ( U. s = ( `' f " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) ) ) } )

This definition is referenced by:  fncvm  31239  iscvm  31241