Description: A continuous function at point P is a mapping. (Contributed by FL, 17-Nov-2006) (Revised by Mario Carneiro, 21-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iscnp2.1 | |- X = U. J |
|
iscnp2.2 | |- Y = U. K |
||
Assertion | cnpf | |- ( F e. ( ( J CnP K ) ` P ) -> F : X --> Y ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscnp2.1 | |- X = U. J |
|
2 | iscnp2.2 | |- Y = U. K |
|
3 | 1 2 | iscnp2 | |- ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. X ) /\ ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |
4 | 3 | simprbi | |- ( F e. ( ( J CnP K ) ` P ) -> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) |
5 | 4 | simpld | |- ( F e. ( ( J CnP K ) ` P ) -> F : X --> Y ) |