Metamath Proof Explorer

Theorem cnf2

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

		Ref	Expression
	Assertion	cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Cn K)) \to F : X ⟶ Y$

Step	Hyp	Ref	Expression
1		iscn	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in K F^{-1} [x] \in J))$
2	1	simprbda	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J Cn K)) \to F : X ⟶ Y$
3	2	3impa	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Cn K)) \to F : X ⟶ Y$