Metamath Proof Explorer

Theorem cvmopn

Description: A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion cvmopn 
|- ( ( F e. ( C CovMap J ) /\ A e. C ) -> ( F " A ) e. J )

Proof

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. C = U. C
3 1 2 cvmopnlem 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> ( F " A ) e. J )