Theorem cnf

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

	Ref	Expression
Hypotheses	iscnp2.1	$$⊢X=\bigcup J$$
	iscnp2.2	$$⊢Y=\bigcup K$$
Assertion	cnf	$$⊢F\in \left(J\mathrm{Cn}K\right)\to F:X⟶Y$$

Proof

Step	Hyp	Ref	Expression
1		iscnp2.1	$$⊢X=\bigcup J$$
2		iscnp2.2	$$⊢Y=\bigcup K$$
3	1 2	iscn2	$$⊢F\in \left(J\mathrm{Cn}K\right)\leftrightarrow \left(\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\wedge \left(F:X⟶Y\wedge \forall x\in K{F}^{-1}\left[x\right]\in J\right)\right)$$
4	3	simprbi	$$⊢F\in \left(J\mathrm{Cn}K\right)\to \left(F:X⟶Y\wedge \forall x\in K{F}^{-1}\left[x\right]\in J\right)$$
5	4	simpld	$$⊢F\in \left(J\mathrm{Cn}K\right)\to F:X⟶Y$$