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 ) ) |
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 ) ) |