Metamath Proof Explorer


Theorem cnpf2

Description: A continuous function at point P is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnpf2
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )

Proof

Step Hyp Ref Expression
1 eqid
 |-  U. J = U. J
2 eqid
 |-  U. K = U. K
3 1 2 cnpf
 |-  ( F e. ( ( J CnP K ) ` P ) -> F : U. J --> U. K )
4 toponuni
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
5 4 feq2d
 |-  ( J e. ( TopOn ` X ) -> ( F : X --> Y <-> F : U. J --> Y ) )
6 toponuni
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
7 6 feq3d
 |-  ( K e. ( TopOn ` Y ) -> ( F : U. J --> Y <-> F : U. J --> U. K ) )
8 5 7 sylan9bb
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F : X --> Y <-> F : U. J --> U. K ) )
9 3 8 syl5ibr
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( ( J CnP K ) ` P ) -> F : X --> Y ) )
10 9 3impia
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )