Theorem cnpf

Description: A continuous function at point P is a mapping. (Contributed by FL, 17-Nov-2006) (Revised by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	iscnp2.1	$$⊢X=\bigcup J$$
	iscnp2.2	$$⊢Y=\bigcup K$$
Assertion	cnpf	$$⊢F\in \left(J\mathrm{CnP}K\right)\left(P\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	iscnp2	$$⊢F\in \left(J\mathrm{CnP}K\right)\left(P\right)\leftrightarrow \left(\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\wedge P\in X\right)\wedge \left(F:X⟶Y\wedge \forall y\in K\left(F\left(P\right)\in y\to \exists x\in J\left(P\in x\wedge F\left[x\right]\subseteq y\right)\right)\right)\right)$$
4	3	simprbi	$$⊢F\in \left(J\mathrm{CnP}K\right)\left(P\right)\to \left(F:X⟶Y\wedge \forall y\in K\left(F\left(P\right)\in y\to \exists x\in J\left(P\in x\wedge F\left[x\right]\subseteq y\right)\right)\right)$$
5	4	simpld	$$⊢F\in \left(J\mathrm{CnP}K\right)\left(P\right)\to F:X⟶Y$$