This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐹 : 𝑋 ⟶ 𝑌 ) )
10 9 3impia ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )