cnpfval

Description: The function mapping the points in a topology J to the set of all functions from J to topology K continuous at that point. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	cnpfval	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J CnP K = (x \in X ⟼ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\})$

Proof

Step	Hyp	Ref	Expression
1		df-cnp	$⊢ CnP = (j \in Top, k \in Top ⟼ (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall w \in k (f (x) \in w \to \exists v \in j (x \in v \land f [v] \subseteq w))\}))$
2	1	a1i	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to CnP = (j \in Top, k \in Top ⟼ (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall w \in k (f (x) \in w \to \exists v \in j (x \in v \land f [v] \subseteq w))\}))$
3		simprl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to j = J$
4	3	unieqd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ⋃ j = ⋃ J$
5		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
6	5	ad2antrr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to X = ⋃ J$
7	4 6	eqtr4d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ⋃ j = X$
8		simprr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to k = K$
9	8	unieqd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ⋃ k = ⋃ K$
10		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
11	10	ad2antlr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to Y = ⋃ K$
12	9 11	eqtr4d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ⋃ k = Y$
13	12 7	oveq12d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to {⋃ k}^{⋃ j} = Y^{X}$
14	3	rexeqdv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to (\exists v \in j (x \in v \land f [v] \subseteq w) \leftrightarrow \exists v \in J (x \in v \land f [v] \subseteq w))$
15	14	imbi2d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to ((f (x) \in w \to \exists v \in j (x \in v \land f [v] \subseteq w)) \leftrightarrow (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w)))$
16	8 15	raleqbidv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to (\forall w \in k (f (x) \in w \to \exists v \in j (x \in v \land f [v] \subseteq w)) \leftrightarrow \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w)))$
17	13 16	rabeqbidv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to \{f \in ({⋃ k}^{⋃ j}) \| \forall w \in k (f (x) \in w \to \exists v \in j (x \in v \land f [v] \subseteq w))\} = \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\}$
18	7 17	mpteq12dv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (j = J \land k = K)) \to (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall w \in k (f (x) \in w \to \exists v \in j (x \in v \land f [v] \subseteq w))\}) = (x \in X ⟼ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\})$
19		topontop	$⊢ J \in TopOn (X) \to J \in Top$
20	19	adantr	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \in Top$
21		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
22	21	adantl	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to K \in Top$
23		ovex	$⊢ Y^{X} \in V$
24		ssrab2	$⊢ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\} \subseteq Y^{X}$
25	23 24	elpwi2	$⊢ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\} \in 𝒫 (Y^{X})$
26	25	a1i	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in X) \to \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\} \in 𝒫 (Y^{X})$
27	26	fmpttd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (x \in X ⟼ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\}) : X ⟶ 𝒫 (Y^{X})$
28		toponmax	$⊢ J \in TopOn (X) \to X \in J$
29	28	adantr	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to X \in J$
30	23	pwex	$⊢ 𝒫 (Y^{X}) \in V$
31	30	a1i	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to 𝒫 (Y^{X}) \in V$
32		fex2	$⊢ ((x \in X ⟼ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\}) : X ⟶ 𝒫 (Y^{X}) \land X \in J \land 𝒫 (Y^{X}) \in V) \to (x \in X ⟼ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\}) \in V$
33	27 29 31 32	syl3anc	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (x \in X ⟼ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\}) \in V$
34	2 18 20 22 33	ovmpod	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J CnP K = (x \in X ⟼ \{f \in (Y^{X}) \| \forall w \in K (f (x) \in w \to \exists v \in J (x \in v \land f [v] \subseteq w))\})$

Metamath Proof Explorer

Theorem cnpfval

Proof