This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ⋃ J
Assertion cnsscnp ⊢ P ∈ X → J Cn K ⊆ J CnP K ⁡ P

Proof

Step Hyp Ref Expression
1 cnsscnp.1 ⊢ X = ⋃ J
2 1 cncnpi ⊢ f ∈ J Cn K ∧ P ∈ X → f ∈ J CnP K ⁡ P
3 2 expcom ⊢ P ∈ X → f ∈ J Cn K → f ∈ J CnP K ⁡ P
4 3 ssrdv ⊢ P ∈ X → J Cn K ⊆ J CnP K ⁡ P