iscnp2

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". Based on Theorem 7.2(g) of Munkres p. 107. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	iscn.1	$⊢ X = ⋃ J$
	iscn.2	$⊢ Y = ⋃ K$
Assertion	iscnp2	$⊢ F \in (J CnP K) (P) \leftrightarrow ((J \in Top \land K \in Top \land P \in X) \land (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$

Proof

Step	Hyp	Ref	Expression
1		iscn.1	$⊢ X = ⋃ J$
2		iscn.2	$⊢ Y = ⋃ K$
3		n0i	$⊢ F \in (J CnP K) (P) \to \neg (J CnP K) (P) = \emptyset$
4		df-ov	$⊢ J CnP K = CnP (⟨J, K⟩)$
5		ndmfv	$⊢ \neg ⟨J, K⟩ \in dom CnP \to CnP (⟨J, K⟩) = \emptyset$
6	4 5	eqtrid	$⊢ \neg ⟨J, K⟩ \in dom CnP \to J CnP K = \emptyset$
7	6	fveq1d	$⊢ \neg ⟨J, K⟩ \in dom CnP \to (J CnP K) (P) = \emptyset (P)$
8		0fv	$⊢ \emptyset (P) = \emptyset$
9	7 8	eqtrdi	$⊢ \neg ⟨J, K⟩ \in dom CnP \to (J CnP K) (P) = \emptyset$
10	3 9	nsyl2	$⊢ F \in (J CnP K) (P) \to ⟨J, K⟩ \in dom CnP$
11		df-cnp	$⊢ CnP = (j \in Top, k \in Top ⟼ (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\}))$
12		ovex	$⊢ {⋃ k}^{⋃ j} \in V$
13		ssrab2	$⊢ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\} \subseteq {⋃ k}^{⋃ j}$
14	12 13	elpwi2	$⊢ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\} \in 𝒫 ({⋃ k}^{⋃ j})$
15	14	rgenw	$⊢ \forall x \in ⋃ j \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\} \in 𝒫 ({⋃ k}^{⋃ j})$
16		eqid	$⊢ (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\}) = (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\})$
17	16	fmpt	$⊢ \forall x \in ⋃ j \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\} \in 𝒫 ({⋃ k}^{⋃ j}) \leftrightarrow (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\}) : ⋃ j ⟶ 𝒫 ({⋃ k}^{⋃ j})$
18	15 17	mpbi	$⊢ (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\}) : ⋃ j ⟶ 𝒫 ({⋃ k}^{⋃ j})$
19		vuniex	$⊢ ⋃ j \in V$
20	12	pwex	$⊢ 𝒫 ({⋃ k}^{⋃ j}) \in V$
21		fex2	$⊢ ((x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\}) : ⋃ j ⟶ 𝒫 ({⋃ k}^{⋃ j}) \land ⋃ j \in V \land 𝒫 ({⋃ k}^{⋃ j}) \in V) \to (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\}) \in V$
22	18 19 20 21	mp3an	$⊢ (x \in ⋃ j ⟼ \{f \in ({⋃ k}^{⋃ j}) \| \forall y \in k (f (x) \in y \to \exists g \in j (x \in g \land f [g] \subseteq y))\}) \in V$
23	11 22	dmmpo	$⊢ dom CnP = Top \times Top$
24	10 23	eleqtrdi	$⊢ F \in (J CnP K) (P) \to ⟨J, K⟩ \in (Top \times Top)$
25		opelxp	$⊢ ⟨J, K⟩ \in (Top \times Top) \leftrightarrow (J \in Top \land K \in Top)$
26	24 25	sylib	$⊢ F \in (J CnP K) (P) \to (J \in Top \land K \in Top)$
27	26	simpld	$⊢ F \in (J CnP K) (P) \to J \in Top$
28	26	simprd	$⊢ F \in (J CnP K) (P) \to K \in Top$
29		elfvdm	$⊢ F \in (J CnP K) (P) \to P \in dom (J CnP K)$
30	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
31	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
32		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))\})$
33	30 31 32	syl2anb	$⊢ (J \in Top \land K \in Top) \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))\})$
34	26 33	syl	$⊢ F \in (J CnP K) (P) \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))\})$
35	34	dmeqd	$⊢ F \in (J CnP K) (P) \to dom (J CnP K) = dom (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))\})$
36		ovex	$⊢ Y^{X} \in V$
37	36	rabex	$⊢ \{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$
38	37	rgenw	$⊢ \forall 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$
39		dmmptg	$⊢ \forall 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 \to dom (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$
40	38 39	ax-mp	$⊢ dom (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$
41	35 40	eqtrdi	$⊢ F \in (J CnP K) (P) \to dom (J CnP K) = X$
42	29 41	eleqtrd	$⊢ F \in (J CnP K) (P) \to P \in X$
43	27 28 42	3jca	$⊢ F \in (J CnP K) (P) \to (J \in Top \land K \in Top \land P \in X)$
44		biid	$⊢ P \in X \leftrightarrow P \in X$
45		iscnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
46	30 31 44 45	syl3anb	$⊢ (J \in Top \land K \in Top \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
47	43 46	biadanii	$⊢ F \in (J CnP K) (P) \leftrightarrow ((J \in Top \land K \in Top \land P \in X) \land (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$

Metamath Proof Explorer

Theorem iscnp2

Proof