cnextucn

Description: Extension by continuity. Proposition 11 of BourbakiTop1 p. II.20. Given a topology J on X , a subset A dense in X , this states a condition for F from A to a space Y Hausdorff and complete to be extensible by continuity. (Contributed by Thierry Arnoux, 4-Dec-2017)

	Ref	Expression
Hypotheses	cnextucn.x	$⊢ X = {Base}_{V}$
	cnextucn.y	$⊢ Y = {Base}_{W}$
	cnextucn.j	$⊢ J = TopOpen (V)$
	cnextucn.k	$⊢ K = TopOpen (W)$
	cnextucn.u	$⊢ U = UnifSt (W)$
	cnextucn.v	$⊢ φ \to V \in TopSp$
	cnextucn.t	$⊢ φ \to W \in TopSp$
	cnextucn.w	$⊢ φ \to W \in CUnifSp$
	cnextucn.h	$⊢ φ \to K \in Haus$
	cnextucn.a	$⊢ φ \to A \subseteq X$
	cnextucn.f	$⊢ φ \to F : A ⟶ Y$
	cnextucn.c	$⊢ φ \to cls (J) (A) = X$
	cnextucn.l	$⊢ (φ \land x \in X) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in CauFilU (U)$
Assertion	cnextucn	$⊢ φ \to (J CnExt K) (F) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		cnextucn.x	$⊢ X = {Base}_{V}$
2		cnextucn.y	$⊢ Y = {Base}_{W}$
3		cnextucn.j	$⊢ J = TopOpen (V)$
4		cnextucn.k	$⊢ K = TopOpen (W)$
5		cnextucn.u	$⊢ U = UnifSt (W)$
6		cnextucn.v	$⊢ φ \to V \in TopSp$
7		cnextucn.t	$⊢ φ \to W \in TopSp$
8		cnextucn.w	$⊢ φ \to W \in CUnifSp$
9		cnextucn.h	$⊢ φ \to K \in Haus$
10		cnextucn.a	$⊢ φ \to A \subseteq X$
11		cnextucn.f	$⊢ φ \to F : A ⟶ Y$
12		cnextucn.c	$⊢ φ \to cls (J) (A) = X$
13		cnextucn.l	$⊢ (φ \land x \in X) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in CauFilU (U)$
14		eqid	$⊢ ⋃ J = ⋃ J$
15		eqid	$⊢ ⋃ K = ⋃ K$
16	3	tpstop	$⊢ V \in TopSp \to J \in Top$
17	6 16	syl	$⊢ φ \to J \in Top$
18	2 4	tpsuni	$⊢ W \in TopSp \to Y = ⋃ K$
19	7 18	syl	$⊢ φ \to Y = ⋃ K$
20	19	feq3d	$⊢ φ \to (F : A ⟶ Y \leftrightarrow F : A ⟶ ⋃ K)$
21	11 20	mpbid	$⊢ φ \to F : A ⟶ ⋃ K$
22	1 3	tpsuni	$⊢ V \in TopSp \to X = ⋃ J$
23	6 22	syl	$⊢ φ \to X = ⋃ J$
24	10 23	sseqtrd	$⊢ φ \to A \subseteq ⋃ J$
25	12 23	eqtrd	$⊢ φ \to cls (J) (A) = ⋃ J$
26	2 4	istps	$⊢ W \in TopSp \leftrightarrow K \in TopOn (Y)$
27	7 26	sylib	$⊢ φ \to K \in TopOn (Y)$
28	27	adantr	$⊢ (φ \land x \in ⋃ J) \to K \in TopOn (Y)$
29	23	eleq2d	$⊢ φ \to (x \in X \leftrightarrow x \in ⋃ J)$
30	29	biimpar	$⊢ (φ \land x \in ⋃ J) \to x \in X$
31	12	adantr	$⊢ (φ \land x \in ⋃ J) \to cls (J) (A) = X$
32	30 31	eleqtrrd	$⊢ (φ \land x \in ⋃ J) \to x \in cls (J) (A)$
33		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
34	17 33	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
35		fveq2	$⊢ X = ⋃ J \to TopOn (X) = TopOn (⋃ J)$
36	35	eleq2d	$⊢ X = ⋃ J \to (J \in TopOn (X) \leftrightarrow J \in TopOn (⋃ J))$
37	23 36	syl	$⊢ φ \to (J \in TopOn (X) \leftrightarrow J \in TopOn (⋃ J))$
38	34 37	mpbird	$⊢ φ \to J \in TopOn (X)$
39	38	adantr	$⊢ (φ \land x \in ⋃ J) \to J \in TopOn (X)$
40	10	adantr	$⊢ (φ \land x \in ⋃ J) \to A \subseteq X$
41		trnei	$⊢ (J \in TopOn (X) \land A \subseteq X \land x \in X) \to (x \in cls (J) (A) \leftrightarrow nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A))$
42	39 40 30 41	syl3anc	$⊢ (φ \land x \in ⋃ J) \to (x \in cls (J) (A) \leftrightarrow nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A))$
43	32 42	mpbid	$⊢ (φ \land x \in ⋃ J) \to nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A)$
44	11	adantr	$⊢ (φ \land x \in ⋃ J) \to F : A ⟶ Y$
45		flfval	$⊢ (K \in TopOn (Y) \land nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ Y) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) = K fLim (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A)$
46	28 43 44 45	syl3anc	$⊢ (φ \land x \in ⋃ J) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) = K fLim (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A)$
47	8	adantr	$⊢ (φ \land x \in ⋃ J) \to W \in CUnifSp$
48	30 13	syldan	$⊢ (φ \land x \in ⋃ J) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in CauFilU (U)$
49	5	fveq2i	$⊢ CauFilU (U) = CauFilU (UnifSt (W))$
50	48 49	eleqtrdi	$⊢ (φ \land x \in ⋃ J) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in CauFilU (UnifSt (W))$
51	2	fvexi	$⊢ Y \in V$
52		filfbas	$⊢ nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \to nei (J) (\{x\}) ↾_{𝑡} A \in fBas (A)$
53	43 52	syl	$⊢ (φ \land x \in ⋃ J) \to nei (J) (\{x\}) ↾_{𝑡} A \in fBas (A)$
54		fmfil	$⊢ (Y \in V \land nei (J) (\{x\}) ↾_{𝑡} A \in fBas (A) \land F : A ⟶ Y) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in Fil (Y)$
55	51 53 44 54	mp3an2i	$⊢ (φ \land x \in ⋃ J) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in Fil (Y)$
56	2 4	cuspcvg	$⊢ (W \in CUnifSp \land (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in CauFilU (UnifSt (W)) \land (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in Fil (Y)) \to K fLim (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \neq \emptyset$
57	47 50 55 56	syl3anc	$⊢ (φ \land x \in ⋃ J) \to K fLim (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \neq \emptyset$
58	46 57	eqnetrd	$⊢ (φ \land x \in ⋃ J) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset$
59		cuspusp	$⊢ W \in CUnifSp \to W \in UnifSp$
60	8 59	syl	$⊢ φ \to W \in UnifSp$
61	4	uspreg	$⊢ (W \in UnifSp \land K \in Haus) \to K \in Reg$
62	60 9 61	syl2anc	$⊢ φ \to K \in Reg$
63	14 15 17 9 21 24 25 58 62	cnextcn	$⊢ φ \to (J CnExt K) (F) \in (J Cn K)$

Metamath Proof Explorer

Theorem cnextucn

Proof