Metamath Proof Explorer

Theorem fncvm

Description: Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Assertion fncvm ⊢ CovMap Fn Top × Top

Proof

Step Hyp Ref Expression
1 df-cvm ⊢ CovMap = c ∈ Top , j ∈ Top ⟼ f ∈ c Cn j | ∀ x ∈ ⋃ j ∃ k ∈ j x ∈ k ∧ ∃ s ∈ 𝒫 c ∖ ∅ ⋃ s = f -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ f ↾ u ∈ c ↾ 𝑡 u Homeo j ↾ 𝑡 k
2 ovex ⊢ c Cn j ∈ V
3 2 rabex ⊢ f ∈ c Cn j | ∀ x ∈ ⋃ j ∃ k ∈ j x ∈ k ∧ ∃ s ∈ 𝒫 c ∖ ∅ ⋃ s = f -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ f ↾ u ∈ c ↾ 𝑡 u Homeo j ↾ 𝑡 k ∈ V
4 1 3 fnmpoi ⊢ CovMap Fn Top × Top