Metamath Proof Explorer


Theorem cnpf

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 )

Proof

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 )