Theorem cnsscnp

Description: The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypothesis	cnsscnp.1	$$⊢X=\bigcup J$$
Assertion	cnsscnp	$$⊢P\in X\to J\mathrm{Cn}K\subseteq \left(J\mathrm{CnP}K\right)\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnsscnp.1	$$⊢X=\bigcup J$$
2	1	cncnpi	$$⊢\left(f\in \left(J\mathrm{Cn}K\right)\wedge P\in X\right)\to f\in \left(J\mathrm{CnP}K\right)\left(P\right)$$
3	2	expcom	$$⊢P\in X\to \left(f\in \left(J\mathrm{Cn}K\right)\to f\in \left(J\mathrm{CnP}K\right)\left(P\right)\right)$$
4	3	ssrdv	$$⊢P\in X\to J\mathrm{Cn}K\subseteq \left(J\mathrm{CnP}K\right)\left(P\right)$$