Description: A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | cvmcn | |- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 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 ) ) ) ) } ) |
|
2 | eqid | |- U. J = U. J |
|
3 | 1 2 | iscvm | |- ( F e. ( C CovMap J ) <-> ( ( C e. Top /\ J e. Top /\ F e. ( C Cn J ) ) /\ A. x e. U. J E. k e. J ( x e. 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 ) ) ) ) } ) ` k ) =/= (/) ) ) ) |
4 | 3 | simplbi | |- ( F e. ( C CovMap J ) -> ( C e. Top /\ J e. Top /\ F e. ( C Cn J ) ) ) |
5 | 4 | simp3d | |- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) ) |