cnextf

Description: Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017)

	Ref	Expression
Hypotheses	cnextf.1	$⊢ C = ⋃ J$
	cnextf.2	$⊢ B = ⋃ K$
	cnextf.3	$⊢ φ \to J \in Top$
	cnextf.4	$⊢ φ \to K \in Haus$
	cnextf.5	$⊢ φ \to F : A ⟶ B$
	cnextf.a	$⊢ φ \to A \subseteq C$
	cnextf.6	$⊢ φ \to cls (J) (A) = C$
	cnextf.7	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset$
Assertion	cnextf	$⊢ φ \to (J CnExt K) (F) : C ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		cnextf.1	$⊢ C = ⋃ J$
2		cnextf.2	$⊢ B = ⋃ K$
3		cnextf.3	$⊢ φ \to J \in Top$
4		cnextf.4	$⊢ φ \to K \in Haus$
5		cnextf.5	$⊢ φ \to F : A ⟶ B$
6		cnextf.a	$⊢ φ \to A \subseteq C$
7		cnextf.6	$⊢ φ \to cls (J) (A) = C$
8		cnextf.7	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset$
9	1 2	cnextfun	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to Fun (J CnExt K) (F)$
10	3 4 5 6 9	syl22anc	$⊢ φ \to Fun (J CnExt K) (F)$
11		dfdm3	$⊢ dom (J CnExt K) (F) = \{x \| \exists y ⟨x, y⟩ \in (J CnExt K) (F)\}$
12		simpl	$⊢ (φ \land x \in C) \to φ$
13	7	eleq2d	$⊢ φ \to (x \in cls (J) (A) \leftrightarrow x \in C)$
14	13	biimpar	$⊢ (φ \land x \in C) \to x \in cls (J) (A)$
15		n0	$⊢ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset \leftrightarrow \exists y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
16	8 15	sylib	$⊢ (φ \land x \in C) \to \exists y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
17		haustop	$⊢ K \in Haus \to K \in Top$
18	4 17	syl	$⊢ φ \to K \in Top$
19	1 2	cnextfval	$⊢ ((J \in Top \land K \in Top) \land (F : A ⟶ B \land A \subseteq C)) \to (J CnExt K) (F) = ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
20	3 18 5 6 19	syl22anc	$⊢ φ \to (J CnExt K) (F) = ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
21	20	eleq2d	$⊢ φ \to (⟨x, y⟩ \in (J CnExt K) (F) \leftrightarrow ⟨x, y⟩ \in ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)))$
22		opeliunxp	$⊢ ⟨x, y⟩ \in ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \leftrightarrow (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
23	21 22	bitrdi	$⊢ φ \to (⟨x, y⟩ \in (J CnExt K) (F) \leftrightarrow (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)))$
24	23	exbidv	$⊢ φ \to (\exists y ⟨x, y⟩ \in (J CnExt K) (F) \leftrightarrow \exists y (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)))$
25		19.42v	$⊢ \exists y (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \leftrightarrow (x \in cls (J) (A) \land \exists y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
26	24 25	bitrdi	$⊢ φ \to (\exists y ⟨x, y⟩ \in (J CnExt K) (F) \leftrightarrow (x \in cls (J) (A) \land \exists y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)))$
27	26	biimpar	$⊢ (φ \land (x \in cls (J) (A) \land \exists y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))) \to \exists y ⟨x, y⟩ \in (J CnExt K) (F)$
28	12 14 16 27	syl12anc	$⊢ (φ \land x \in C) \to \exists y ⟨x, y⟩ \in (J CnExt K) (F)$
29	26	simprbda	$⊢ (φ \land \exists y ⟨x, y⟩ \in (J CnExt K) (F)) \to x \in cls (J) (A)$
30	13	adantr	$⊢ (φ \land \exists y ⟨x, y⟩ \in (J CnExt K) (F)) \to (x \in cls (J) (A) \leftrightarrow x \in C)$
31	29 30	mpbid	$⊢ (φ \land \exists y ⟨x, y⟩ \in (J CnExt K) (F)) \to x \in C$
32	28 31	impbida	$⊢ φ \to (x \in C \leftrightarrow \exists y ⟨x, y⟩ \in (J CnExt K) (F))$
33	32	abbi2dv	$⊢ φ \to C = \{x \| \exists y ⟨x, y⟩ \in (J CnExt K) (F)\}$
34	11 33	eqtr4id	$⊢ φ \to dom (J CnExt K) (F) = C$
35		df-fn	$⊢ (J CnExt K) (F) Fn C \leftrightarrow (Fun (J CnExt K) (F) \land dom (J CnExt K) (F) = C)$
36	10 34 35	sylanbrc	$⊢ φ \to (J CnExt K) (F) Fn C$
37	20	rneqd	$⊢ φ \to ran (J CnExt K) (F) = ran ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
38		rniun	$⊢ ran ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) = ⋃_{x \in cls (J) (A)} ran (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
39		vex	$⊢ x \in V$
40	39	snnz	$⊢ \{x\} \neq \emptyset$
41		rnxp	$⊢ \{x\} \neq \emptyset \to ran (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) = (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
42	40 41	ax-mp	$⊢ ran (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) = (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
43	13	biimpa	$⊢ (φ \land x \in cls (J) (A)) \to x \in C$
44	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (B)$
45	18 44	sylib	$⊢ φ \to K \in TopOn (B)$
46	45	adantr	$⊢ (φ \land x \in C) \to K \in TopOn (B)$
47	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (C)$
48	3 47	sylib	$⊢ φ \to J \in TopOn (C)$
49	48	adantr	$⊢ (φ \land x \in C) \to J \in TopOn (C)$
50	6	adantr	$⊢ (φ \land x \in C) \to A \subseteq C$
51		simpr	$⊢ (φ \land x \in C) \to x \in C$
52		trnei	$⊢ (J \in TopOn (C) \land A \subseteq C \land x \in C) \to (x \in cls (J) (A) \leftrightarrow nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A))$
53	52	biimpa	$⊢ ((J \in TopOn (C) \land A \subseteq C \land x \in C) \land x \in cls (J) (A)) \to nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A)$
54	49 50 51 14 53	syl31anc	$⊢ (φ \land x \in C) \to nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A)$
55	5	adantr	$⊢ (φ \land x \in C) \to F : A ⟶ B$
56		flfelbas	$⊢ ((K \in TopOn (B) \land nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \to y \in B$
57	56	ex	$⊢ (K \in TopOn (B) \land nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \to (y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \to y \in B)$
58	57	ssrdv	$⊢ (K \in TopOn (B) \land nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \subseteq B$
59	46 54 55 58	syl3anc	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \subseteq B$
60	43 59	syldan	$⊢ (φ \land x \in cls (J) (A)) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \subseteq B$
61	42 60	eqsstrid	$⊢ (φ \land x \in cls (J) (A)) \to ran (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \subseteq B$
62	61	ralrimiva	$⊢ φ \to \forall x \in cls (J) (A) ran (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \subseteq B$
63		iunss	$⊢ ⋃_{x \in cls (J) (A)} ran (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \subseteq B \leftrightarrow \forall x \in cls (J) (A) ran (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \subseteq B$
64	62 63	sylibr	$⊢ φ \to ⋃_{x \in cls (J) (A)} ran (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \subseteq B$
65	38 64	eqsstrid	$⊢ φ \to ran ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \subseteq B$
66	37 65	eqsstrd	$⊢ φ \to ran (J CnExt K) (F) \subseteq B$
67		df-f	$⊢ (J CnExt K) (F) : C ⟶ B \leftrightarrow ((J CnExt K) (F) Fn C \land ran (J CnExt K) (F) \subseteq B)$
68	36 66 67	sylanbrc	$⊢ φ \to (J CnExt K) (F) : C ⟶ B$

Metamath Proof Explorer

Theorem cnextf

Proof