Theorem cvmtop2

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

	Ref	Expression
Assertion	cvmtop2	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ¬ ( 𝐶 CovMap 𝐽 ) = ∅ )
2		fncvm	⊢ CovMap Fn ( Top × Top )
3	2	fndmi	⊢ dom CovMap = ( Top × Top )
4	3	ndmov	⊢ ( ¬ ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐶 CovMap 𝐽 ) = ∅ )
5	1 4	nsyl2	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) )
6	5	simprd	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐽 ∈ Top )