Metamath Proof Explorer

Theorem cnf2

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

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

Proof

Step Hyp Ref Expression
1 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
2 1 simprbda 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> F : X --> Y )
3 2 3impa 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Cn K ) ) -> F : X --> Y )