Metamath Proof Explorer

Theorem cvmtop2

Description: Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Assertion cvmtop2 
|- ( F e. ( C CovMap J ) -> J e. Top )

Proof

Step Hyp Ref Expression
1 n0i 
 |-  ( F e. ( C CovMap J ) -> -. ( C CovMap J ) = (/) )
2 fncvm 
 |-  CovMap Fn ( Top X. Top )
3 2 fndmi 
 |-  dom CovMap = ( Top X. Top )
4 3 ndmov 
 |-  ( -. ( C e. Top /\ J e. Top ) -> ( C CovMap J ) = (/) )
5 1 4 nsyl2 
 |-  ( F e. ( C CovMap J ) -> ( C e. Top /\ J e. Top ) )
6 5 simprd 
 |-  ( F e. ( C CovMap J ) -> J e. Top )