Theorem cnpcl

Description: The value of a continuous function from J to K at point P belongs to the underlying set of topology K . (Contributed by FL, 27-Dec-2006) (Revised by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	iscnp2.1	$$⊢X=\bigcup J$$
	iscnp2.2	$$⊢Y=\bigcup K$$
Assertion	cnpcl	$$⊢\left(F\in \left(J\mathrm{CnP}K\right)\left(P\right)\wedge A\in X\right)\to F\left(A\right)\in Y$$

Proof

Step	Hyp	Ref	Expression
1		iscnp2.1	$$⊢X=\bigcup J$$
2		iscnp2.2	$$⊢Y=\bigcup K$$
3	1 2	cnpf	$$⊢F\in \left(J\mathrm{CnP}K\right)\left(P\right)\to F:X⟶Y$$
4	3	ffvelrnda	$$⊢\left(F\in \left(J\mathrm{CnP}K\right)\left(P\right)\wedge A\in X\right)\to F\left(A\right)\in Y$$