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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋𝑌 )

Proof

Step Hyp Ref Expression
1 eqid 𝐽 = 𝐽
2 eqid 𝐾 = 𝐾
3 1 2 cnpf ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐹 : 𝐽 𝐾 )
4 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
5 4 feq2d ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐹 : 𝑋𝑌𝐹 : 𝐽𝑌 ) )
6 toponuni ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = 𝐾 )
7 6 feq3d ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → ( 𝐹 : 𝐽𝑌𝐹 : 𝐽 𝐾 ) )
8 5 7 sylan9bb ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 : 𝑋𝑌𝐹 : 𝐽 𝐾 ) )
9 3 8 syl5ibr ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐹 : 𝑋𝑌 ) )
10 9 3impia ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋𝑌 )