cnextfun

Description: If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017)

	Ref	Expression
Hypotheses	cnextfrel.1	$⊢ C = ⋃ J$
	cnextfrel.2	$⊢ B = ⋃ K$
Assertion	cnextfun	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to Fun (J CnExt K) (F)$

Proof

Step	Hyp	Ref	Expression
1		cnextfrel.1	$⊢ C = ⋃ J$
2		cnextfrel.2	$⊢ B = ⋃ K$
3		haustop	$⊢ K \in Haus \to K \in Top$
4	1 2	cnextrel	$⊢ ((J \in Top \land K \in Top) \land (F : A ⟶ B \land A \subseteq C)) \to Rel (J CnExt K) (F)$
5	3 4	sylanl2	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to Rel (J CnExt K) (F)$
6		simpllr	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to K \in Haus$
7	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (C)$
8	7	biimpi	$⊢ J \in Top \to J \in TopOn (C)$
9	8	ad3antrrr	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to J \in TopOn (C)$
10		simplrr	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to A \subseteq C$
11	9 7	sylibr	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to J \in Top$
12	1	clsss3	$⊢ (J \in Top \land A \subseteq C) \to cls (J) (A) \subseteq C$
13	11 10 12	syl2anc	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to cls (J) (A) \subseteq C$
14		simpr	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to x \in cls (J) (A)$
15	13 14	sseldd	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to x \in C$
16		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))$
17	16	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)$
18	9 10 15 14 17	syl31anc	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A)$
19		simplrl	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to F : A ⟶ B$
20	2	hausflf	$⊢ (K \in Haus \land nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \to \exists^{*} y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
21	6 18 19 20	syl3anc	$⊢ (((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \land x \in cls (J) (A)) \to \exists^{*} y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
22	21	ex	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to (x \in cls (J) (A) \to \exists^{*} y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
23	22	alrimiv	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to \forall x (x \in cls (J) (A) \to \exists^{*} y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
24		moanimv	$⊢ \exists^{} y (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \leftrightarrow (x \in cls (J) (A) \to \exists^{} y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
25	24	albii	$⊢ \forall x \exists^{} y (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \leftrightarrow \forall x (x \in cls (J) (A) \to \exists^{} y y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
26	23 25	sylibr	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to \forall x \exists^{*} y (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
27		df-br	$⊢ x (J CnExt K) (F) y \leftrightarrow ⟨x, y⟩ \in (J CnExt K) (F)$
28	27	a1i	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to (x (J CnExt K) (F) y \leftrightarrow ⟨x, y⟩ \in (J CnExt K) (F))$
29	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))$
30	3 29	sylanl2	$⊢ ((J \in Top \land K \in Haus) \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))$
31	30	eleq2d	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \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)))$
32		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))$
33	32	a1i	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to (⟨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)))$
34	28 31 33	3bitrd	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to (x (J CnExt K) (F) y \leftrightarrow (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)))$
35	34	mobidv	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to (\exists^{} y x (J CnExt K) (F) y \leftrightarrow \exists^{} y (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)))$
36	35	albidv	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to (\forall x \exists^{} y x (J CnExt K) (F) y \leftrightarrow \forall x \exists^{} y (x \in cls (J) (A) \land y \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)))$
37	26 36	mpbird	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to \forall x \exists^{*} y x (J CnExt K) (F) y$
38		dffun6	$⊢ Fun (J CnExt K) (F) \leftrightarrow (Rel (J CnExt K) (F) \land \forall x \exists^{*} y x (J CnExt K) (F) y)$
39	5 37 38	sylanbrc	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to Fun (J CnExt K) (F)$

Metamath Proof Explorer

Theorem cnextfun

Proof