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