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 = U. J |
|
| iscnp2.2 | |- Y = U. K |
||
| Assertion | cnpcl | |- ( ( F e. ( ( J CnP K ) ` P ) /\ A e. X ) -> ( F ` A ) e. Y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iscnp2.1 | |- X = U. J |
|
| 2 | iscnp2.2 | |- Y = U. K |
|
| 3 | 1 2 | cnpf | |- ( F e. ( ( J CnP K ) ` P ) -> F : X --> Y ) |
| 4 | 3 | ffvelrnda | |- ( ( F e. ( ( J CnP K ) ` P ) /\ A e. X ) -> ( F ` A ) e. Y ) |