Metamath Proof Explorer

Theorem cnpf2

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

Ref Expression
Assertion cnpf2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J CnP K ⁡ P → F : X ⟶ Y

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 eqid ⊢ ⋃ K = ⋃ K
3 1 2 cnpf ⊢ F ∈ J CnP K ⁡ P → F : ⋃ J ⟶ ⋃ K
4 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
5 4 feq2d ⊢ J ∈ TopOn ⁡ X → F : X ⟶ Y ↔ F : ⋃ J ⟶ Y
6 toponuni ⊢ K ∈ TopOn ⁡ Y → Y = ⋃ K
7 6 feq3d ⊢ K ∈ TopOn ⁡ Y → F : ⋃ J ⟶ Y ↔ F : ⋃ J ⟶ ⋃ K
8 5 7 sylan9bb ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F : X ⟶ Y ↔ F : ⋃ J ⟶ ⋃ K
9 3 8 imbitrrid ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J CnP K ⁡ P → F : X ⟶ Y
10 9 3impia ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J CnP K ⁡ P → F : X ⟶ Y