Theorem cnf

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

	Ref	Expression
Hypotheses	iscnp2.1	|- X = U. J
	iscnp2.2	|- Y = U. K
Assertion	cnf	|- ( F e. ( J Cn K ) -> F : X --> Y )

Proof

Step	Hyp	Ref	Expression
1		iscnp2.1	|- X = U. J
2		iscnp2.2	|- Y = U. K
3	1 2	iscn2	|- ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
4	3	simprbi	|- ( F e. ( J Cn K ) -> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) )
5	4	simpld	|- ( F e. ( J Cn K ) -> F : X --> Y )