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 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )