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	⊢ 𝑋 = ∪ 𝐽
Assertion	cnsscnp	⊢ ( 𝑃 ∈ 𝑋 → ( 𝐽 Cn 𝐾 ) ⊆ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		cnsscnp.1	⊢ 𝑋 = ∪ 𝐽
2	1	cncnpi	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
3	2	expcom	⊢ ( 𝑃 ∈ 𝑋 → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝑓 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) )
4	3	ssrdv	⊢ ( 𝑃 ∈ 𝑋 → ( 𝐽 Cn 𝐾 ) ⊆ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )