Metamath Proof Explorer

Theorem cvmcn

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

Ref Expression
Assertion cvmcn ⊢ F ∈ C CovMap J → F ∈ C Cn J

Proof

Step Hyp Ref Expression
1 eqid ⊢ k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
2 eqid ⊢ ⋃ J = ⋃ J
3 1 2 iscvm ⊢ F ∈ C CovMap J ↔ C ∈ Top ∧ J ∈ Top ∧ F ∈ C Cn J ∧ ∀ x ∈ ⋃ J ∃ k ∈ J x ∈ k ∧ k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k ⁡ k ≠ ∅
4 3 simplbi ⊢ F ∈ C CovMap J → C ∈ Top ∧ J ∈ Top ∧ F ∈ C Cn J
5 4 simp3d ⊢ F ∈ C CovMap J → F ∈ C Cn J