Theorem cvmfo

Description: A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypotheses	cvmlift.1	|- B = U. C
	cvmfo.2	|- X = U. J
Assertion	cvmfo	|- ( F e. ( C CovMap J ) -> F : B -onto-> X )

Proof

Step	Hyp	Ref	Expression
1		cvmlift.1	|- B = U. C
2		cvmfo.2	|- X = U. J
3		eqid	|- ( k e. J |-> { 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 ) ) ) ) } ) = ( k e. J |-> { 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 ) ) ) ) } )
4	3	cvmscbv	|- ( k e. J |-> { 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 ) ) ) ) } ) = ( a e. J |-> { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) } )
5	4 1 2	cvmfolem	|- ( F e. ( C CovMap J ) -> F : B -onto-> X )