cnfval

Description: The set of all continuous functions from topology J to topology K . (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	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\}$

Proof

Step	Hyp	Ref	Expression
1		df-cn	$⊢ Cn = (j \in Top, k \in Top ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k f^{-1} [y] \in j\})$
2	1	a1i	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to Cn = (j \in Top, k \in Top ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k f^{-1} [y] \in j\})$
3		simprr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to k = K$
4	3	unieqd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ⋃ k = ⋃ K$
5		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
6	5	ad2antlr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to Y = ⋃ K$
7	4 6	eqtr4d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ⋃ k = Y$
8		simprl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to j = J$
9	8	unieqd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ⋃ j = ⋃ J$
10		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
11	10	ad2antrr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to X = ⋃ J$
12	9 11	eqtr4d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ⋃ j = X$
13	7 12	oveq12d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to {⋃ k}^{⋃ j} = Y^{X}$
14	8	eleq2d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to (f^{-1} [y] \in j \leftrightarrow f^{-1} [y] \in J)$
15	3 14	raleqbidv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to (\forall y \in k f^{-1} [y] \in j \leftrightarrow \forall y \in K f^{-1} [y] \in J)$
16	13 15	rabeqbidv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k f^{-1} [y] \in j\} = \{f \in (Y^{X}) \| \forall y \in K f^{-1} [y] \in J\}$
17		topontop	$⊢ J \in TopOn (X) \to J \in Top$
18	17	adantr	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \in Top$
19		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
20	19	adantl	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to K \in Top$
21		ovex	$⊢ Y^{X} \in V$
22	21	rabex	$⊢ \{f \in (Y^{X}) \| \forall y \in K f^{-1} [y] \in J\} \in V$
23	22	a1i	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to \{f \in (Y^{X}) \| \forall y \in K f^{-1} [y] \in J\} \in V$
24	2 16 18 20 23	ovmpod	$⊢ (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\}$

Metamath Proof Explorer

Theorem cnfval

Proof