This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Topology Limits and continuity in topological spaces 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 𝐾 ) ‘ 𝑃 ) )