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 imbitrrid 
 |-  ( ( 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 )