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 = U. J
Assertion cnsscnp
|- ( P e. X -> ( J Cn K ) C_ ( ( J CnP K ) ` P ) )

Proof

Step Hyp Ref Expression
1 cnsscnp.1
 |-  X = U. J
2 1 cncnpi
 |-  ( ( f e. ( J Cn K ) /\ P e. X ) -> f e. ( ( J CnP K ) ` P ) )
3 2 expcom
 |-  ( P e. X -> ( f e. ( J Cn K ) -> f e. ( ( J CnP K ) ` P ) ) )
4 3 ssrdv
 |-  ( P e. X -> ( J Cn K ) C_ ( ( J CnP K ) ` P ) )