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 ffvelrnda F J CnP K P A X F A Y