Metamath Proof Explorer


Theorem 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 φ V TopSp
cnextucn.t φ W TopSp
cnextucn.w φ W CUnifSp
cnextucn.h φ K Haus
cnextucn.a φ A X
cnextucn.f φ F : A Y
cnextucn.c φ cls J A = X
cnextucn.l φ x X Y FilMap F nei J x 𝑡 A CauFilU U
Assertion cnextucn φ J CnExt K F 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 φ V TopSp
7 cnextucn.t φ W TopSp
8 cnextucn.w φ W CUnifSp
9 cnextucn.h φ K Haus
10 cnextucn.a φ A X
11 cnextucn.f φ F : A Y
12 cnextucn.c φ cls J A = X
13 cnextucn.l φ x X Y FilMap F nei J x 𝑡 A CauFilU U
14 eqid J = J
15 eqid K = K
16 3 tpstop V TopSp J Top
17 6 16 syl φ J Top
18 2 4 tpsuni W TopSp Y = K
19 7 18 syl φ Y = K
20 19 feq3d φ F : A Y F : A K
21 11 20 mpbid φ F : A K
22 1 3 tpsuni V TopSp X = J
23 6 22 syl φ X = J
24 10 23 sseqtrd φ A J
25 12 23 eqtrd φ cls J A = J
26 2 4 istps W TopSp K TopOn Y
27 7 26 sylib φ K TopOn Y
28 27 adantr φ x J K TopOn Y
29 23 eleq2d φ x X x J
30 29 biimpar φ x J x X
31 12 adantr φ x J cls J A = X
32 30 31 eleqtrrd φ x J x cls J A
33 toptopon2 J Top J TopOn J
34 17 33 sylib φ J TopOn J
35 fveq2 X = J TopOn X = TopOn J
36 35 eleq2d X = J J TopOn X J TopOn J
37 23 36 syl φ J TopOn X J TopOn J
38 34 37 mpbird φ J TopOn X
39 38 adantr φ x J J TopOn X
40 10 adantr φ x J A X
41 trnei J TopOn X A X x X x cls J A nei J x 𝑡 A Fil A
42 39 40 30 41 syl3anc φ x J x cls J A nei J x 𝑡 A Fil A
43 32 42 mpbid φ x J nei J x 𝑡 A Fil A
44 11 adantr φ x J F : A Y
45 flfval K TopOn Y nei J x 𝑡 A Fil A F : A Y K fLimf nei J x 𝑡 A F = K fLim Y FilMap F nei J x 𝑡 A
46 28 43 44 45 syl3anc φ x J K fLimf nei J x 𝑡 A F = K fLim Y FilMap F nei J x 𝑡 A
47 8 adantr φ x J W CUnifSp
48 30 13 syldan φ x J Y FilMap F nei J x 𝑡 A CauFilU U
49 5 fveq2i CauFilU U = CauFilU UnifSt W
50 48 49 eleqtrdi φ x J Y FilMap F nei J x 𝑡 A CauFilU UnifSt W
51 2 fvexi Y V
52 filfbas nei J x 𝑡 A Fil A nei J x 𝑡 A fBas A
53 43 52 syl φ x J nei J x 𝑡 A fBas A
54 fmfil Y V nei J x 𝑡 A fBas A F : A Y Y FilMap F nei J x 𝑡 A Fil Y
55 51 53 44 54 mp3an2i φ x J Y FilMap F nei J x 𝑡 A Fil Y
56 2 4 cuspcvg W CUnifSp Y FilMap F nei J x 𝑡 A CauFilU UnifSt W Y FilMap F nei J x 𝑡 A Fil Y K fLim Y FilMap F nei J x 𝑡 A
57 47 50 55 56 syl3anc φ x J K fLim Y FilMap F nei J x 𝑡 A
58 46 57 eqnetrd φ x J K fLimf nei J x 𝑡 A F
59 cuspusp W CUnifSp W UnifSp
60 8 59 syl φ W UnifSp
61 4 uspreg W UnifSp K Haus K Reg
62 60 9 61 syl2anc φ K Reg
63 14 15 17 9 21 24 25 58 62 cnextcn φ J CnExt K F J Cn K