Metamath Proof Explorer

Theorem cvmfo

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

Ref Expression
Hypotheses cvmlift.1 ⊢ B = ⋃ C
cvmfo.2 ⊢ X = ⋃ J
Assertion cvmfo ⊢ F ∈ C CovMap J → F : B ⟶ onto X

Proof

Step Hyp Ref Expression
1 cvmlift.1 ⊢ B = ⋃ C
2 cvmfo.2 ⊢ X = ⋃ J
3 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
4 3 cvmscbv ⊢ k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k = a ∈ J ⟼ b ∈ 𝒫 C ∖ ∅ | ⋃ b = F -1 a ∧ ∀ c ∈ b ∀ d ∈ b ∖ c c ∩ d = ∅ ∧ F ↾ c ∈ C ↾ 𝑡 c Homeo J ↾ 𝑡 a
5 4 1 2 cvmfolem ⊢ F ∈ C CovMap J → F : B ⟶ onto X