Metamath Proof Explorer

Theorem cvmtop2

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

Ref Expression
Assertion cvmtop2 ⊢ F ∈ C CovMap J → J ∈ Top

Proof

Step Hyp Ref Expression
1 n0i ⊢ F ∈ C CovMap J → ¬ C CovMap J = ∅
2 fncvm ⊢ CovMap Fn Top × Top
3 fndm ⊢ CovMap Fn Top × Top → dom ⁡ CovMap = Top × Top
4 2 3 ax-mp ⊢ dom ⁡ CovMap = Top × Top
5 4 ndmov ⊢ ¬ C ∈ Top ∧ J ∈ Top → C CovMap J = ∅
6 1 5 nsyl2 ⊢ F ∈ C CovMap J → C ∈ Top ∧ J ∈ Top
7 6 simprd ⊢ F ∈ C CovMap J → J ∈ Top