Theorem cvmtop1

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

	Ref	Expression
Assertion	cvmtop1	$$⊢F\in \left(C\mathrm{CovMap}J\right)\to C\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢F\in \left(C\mathrm{CovMap}J\right)\to \neg C\mathrm{CovMap}J=\varnothing$$
2		fncvm	$$⊢\mathrm{CovMap}Fn\left(\mathrm{Top}\times \mathrm{Top}\right)$$
3	2	fndmi	$$⊢\mathrm{dom}\mathrm{CovMap}=\mathrm{Top}\times \mathrm{Top}$$
4	3	ndmov	$$⊢\neg \left(C\in \mathrm{Top}\wedge J\in \mathrm{Top}\right)\to C\mathrm{CovMap}J=\varnothing$$
5	1 4	nsyl2	$$⊢F\in \left(C\mathrm{CovMap}J\right)\to \left(C\in \mathrm{Top}\wedge J\in \mathrm{Top}\right)$$
6	5	simpld	$$⊢F\in \left(C\mathrm{CovMap}J\right)\to C\in \mathrm{Top}$$