Metamath Proof Explorer

Theorem cnf2

Description: A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnf2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Cn K → F : X ⟶ Y

Proof

Step Hyp Ref Expression
1 iscn ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ K F -1 x ∈ J
2 1 simprbda ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Cn K → F : X ⟶ Y
3 2 3impa ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Cn K → F : X ⟶ Y