Metamath Proof Explorer

Theorem iscn

Description: The predicate "the class F is a continuous function from topology J to topology K ". Definition of continuous function in Munkres p. 102. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	iscn	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$

Proof

Step	Hyp	Ref	Expression
1		cnfval	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J Cn K = \{f \in (Y^{X}) \| \forall y \in K f^{-1} [y] \in J\}$
2	1	eleq2d	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow F \in \{f \in (Y^{X}) \| \forall y \in K f^{-1} [y] \in J\})$
3		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
4	3	imaeq1d	$⊢ f = F \to f^{-1} [y] = F^{-1} [y]$
5	4	eleq1d	$⊢ f = F \to (f^{-1} [y] \in J \leftrightarrow F^{-1} [y] \in J)$
6	5	ralbidv	$⊢ f = F \to (\forall y \in K f^{-1} [y] \in J \leftrightarrow \forall y \in K F^{-1} [y] \in J)$
7	6	elrab	$⊢ F \in \{f \in (Y^{X}) \| \forall y \in K f^{-1} [y] \in J\} \leftrightarrow (F \in (Y^{X}) \land \forall y \in K F^{-1} [y] \in J)$
8		toponmax	$⊢ K \in TopOn (Y) \to Y \in K$
9		toponmax	$⊢ J \in TopOn (X) \to X \in J$
10		elmapg	$⊢ (Y \in K \land X \in J) \to (F \in (Y^{X}) \leftrightarrow F : X ⟶ Y)$
11	8 9 10	syl2anr	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (Y^{X}) \leftrightarrow F : X ⟶ Y)$
12	11	anbi1d	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F \in (Y^{X}) \land \forall y \in K F^{-1} [y] \in J) \leftrightarrow (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$
13	7 12	bitrid	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in \{f \in (Y^{X}) \| \forall y \in K f^{-1} [y] \in J\} \leftrightarrow (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$
14	2 13	bitrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$