Theorem cnf2

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

	Ref	Expression
Assertion	cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		iscn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
2	1	simprbda	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
3	2	3impa	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )