Theorem fncvm

Description: Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Assertion	fncvm	|- CovMap Fn ( Top X. Top )

Proof

Step	Hyp	Ref	Expression
1		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 ) ) ) ) ) } )
2		ovex	|- ( c Cn j ) e. _V
3	2	rabex	|- { 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 ) ) ) ) ) } e. _V
4	1 3	fnmpoi	|- CovMap Fn ( Top X. Top )