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

Metamath Proof Explorer

Theorem cnpcl

Description: The value of a continuous function from J to K at point P belongs to the underlying set of topology K . (Contributed by FL, 27-Dec-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses iscnp2.1 ⊢ X = ⋃ J
iscnp2.2 ⊢ Y = ⋃ K
Assertion cnpcl ⊢ F ∈ J CnP K ⁡ P ∧ A ∈ X → F ⁡ A ∈ Y

Proof

Step Hyp Ref Expression
1 iscnp2.1 ⊢ X = ⋃ J
2 iscnp2.2 ⊢ Y = ⋃ K
3 1 2 cnpf ⊢ F ∈ J CnP K ⁡ P → F : X ⟶ Y
4 3 ffvelcdmda ⊢ F ∈ J CnP K ⁡ P ∧ A ∈ X → F ⁡ A ∈ Y