Metamath Proof Explorer

Theorem iscn2

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 Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Hypotheses	iscn.1	$⊢ X = ⋃ J$
		iscn.2	$⊢ Y = ⋃ K$
	Assertion	iscn2	$⊢ F \in (J Cn K) \leftrightarrow ((J \in Top \land K \in Top) \land (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$

Proof

Step	Hyp	Ref	Expression
1		iscn.1	$⊢ X = ⋃ J$
2		iscn.2	$⊢ Y = ⋃ K$
3		df-cn	$⊢ Cn = (j \in Top, k \in Top ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k f^{-1} [y] \in j\})$
4	3	elmpocl	$⊢ F \in (J Cn K) \to (J \in Top \land K \in Top)$
5	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
6	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
7		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))$
8	5 6 7	syl2anb	$⊢ (J \in Top \land K \in Top) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$
9	4 8	biadanii	$⊢ F \in (J Cn K) \leftrightarrow ((J \in Top \land K \in Top) \land (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$