cvmtop1

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

		Ref	Expression
	Assertion	cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$

Step	Hyp	Ref	Expression
1		n0i	$⊢ F \in (C CovMap J) \to \neg C CovMap J = \emptyset$
2		fncvm	$⊢ CovMap Fn (Top \times Top)$
3	2	fndmi	$⊢ dom CovMap = Top \times Top$
4	3	ndmov	$⊢ \neg (C \in Top \land J \in Top) \to C CovMap J = \emptyset$
5	1 4	nsyl2	$⊢ F \in (C CovMap J) \to (C \in Top \land J \in Top)$
6	5	simpld	$⊢ F \in (C CovMap J) \to C \in Top$

Metamath Proof Explorer