cvmcn

Description: A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015)

		Ref	Expression
	Assertion	cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\}) = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	1 2	iscvm	$⊢ F \in (C CovMap J) \leftrightarrow ((C \in Top \land J \in Top \land F \in (C Cn J)) \land \forall x \in ⋃ J \exists k \in J (x \in k \land (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\}) (k) \neq \emptyset))$
4	3	simplbi	$⊢ F \in (C CovMap J) \to (C \in Top \land J \in Top \land F \in (C Cn J))$
5	4	simp3d	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$

Metamath Proof Explorer