Metamath Proof Explorer

Theorem ucnextcn

Description: Extension by continuity. Theorem 2 of BourbakiTop1 p. II.20. Given an uniform space on a set X , a subset A dense in X , and a function F uniformly continuous from A to Y , that function can be extended by continuity to the whole X , and its extension is uniformly continuous. (Contributed by Thierry Arnoux, 25-Jan-2018)

Ref Expression
Hypotheses ucnextcn.x ⊢ 𝑋 = ( Base ‘ 𝑉 )
ucnextcn.y ⊢ 𝑌 = ( Base ‘ 𝑊 )
ucnextcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑉 )
ucnextcn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑊 )
ucnextcn.s ⊢ 𝑆 = ( UnifSt ‘ 𝑉 )
ucnextcn.t ⊢ 𝑇 = ( UnifSt ‘ ( 𝑉 ↾s 𝐴 ) )
ucnextcn.u ⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
ucnextcn.v ⊢ ( 𝜑 → 𝑉 ∈ TopSp )
ucnextcn.r ⊢ ( 𝜑 → 𝑉 ∈ UnifSp )
ucnextcn.w ⊢ ( 𝜑 → 𝑊 ∈ TopSp )
ucnextcn.z ⊢ ( 𝜑 → 𝑊 ∈ CUnifSp )
ucnextcn.h ⊢ ( 𝜑 → 𝐾 ∈ Haus )
ucnextcn.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
ucnextcn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑇 Cnu 𝑈 ) )
ucnextcn.c ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
Assertion ucnextcn ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 ucnextcn.x ⊢ 𝑋 = ( Base ‘ 𝑉 )
2 ucnextcn.y ⊢ 𝑌 = ( Base ‘ 𝑊 )
3 ucnextcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑉 )
4 ucnextcn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑊 )
5 ucnextcn.s ⊢ 𝑆 = ( UnifSt ‘ 𝑉 )
6 ucnextcn.t ⊢ 𝑇 = ( UnifSt ‘ ( 𝑉 ↾s 𝐴 ) )
7 ucnextcn.u ⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
8 ucnextcn.v ⊢ ( 𝜑 → 𝑉 ∈ TopSp )
9 ucnextcn.r ⊢ ( 𝜑 → 𝑉 ∈ UnifSp )
10 ucnextcn.w ⊢ ( 𝜑 → 𝑊 ∈ TopSp )
11 ucnextcn.z ⊢ ( 𝜑 → 𝑊 ∈ CUnifSp )
12 ucnextcn.h ⊢ ( 𝜑 → 𝐾 ∈ Haus )
13 ucnextcn.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
14 ucnextcn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑇 Cnu 𝑈 ) )
15 ucnextcn.c ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
16 1 6 ressust ⊢ ( ( 𝑉 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋 ) → 𝑇 ∈ ( UnifOn ‘ 𝐴 ) )
17 9 13 16 syl2anc ⊢ ( 𝜑 → 𝑇 ∈ ( UnifOn ‘ 𝐴 ) )
18 cuspusp ⊢ ( 𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp )
19 11 18 syl ⊢ ( 𝜑 → 𝑊 ∈ UnifSp )
20 2 7 4 isusp ⊢ ( 𝑊 ∈ UnifSp ↔ ( 𝑈 ∈ ( UnifOn ‘ 𝑌 ) ∧ 𝐾 = ( unifTop ‘ 𝑈 ) ) )
21 19 20 sylib ⊢ ( 𝜑 → ( 𝑈 ∈ ( UnifOn ‘ 𝑌 ) ∧ 𝐾 = ( unifTop ‘ 𝑈 ) ) )
22 21 simpld ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑌 ) )
23 isucn ⊢ ( ( 𝑇 ∈ ( UnifOn ‘ 𝐴 ) ∧ 𝑈 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑇 Cnu 𝑈 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑣 𝑧 → ( 𝐹 ‘ 𝑦 ) 𝑤 ( 𝐹 ‘ 𝑧 ) ) ) ) )
24 17 22 23 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑇 Cnu 𝑈 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑣 𝑧 → ( 𝐹 ‘ 𝑦 ) 𝑤 ( 𝐹 ‘ 𝑧 ) ) ) ) )
25 14 24 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ 𝑈 ∃ 𝑣 ∈ 𝑇 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑣 𝑧 → ( 𝐹 ‘ 𝑦 ) 𝑤 ( 𝐹 ‘ 𝑧 ) ) ) )
26 25 simpld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑌 )
27 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑈 ∈ ( UnifOn ‘ 𝑌 ) )
28 27 elfvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑌 ∈ V )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
30 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
31 29 30 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
32 1 3 istps ⊢ ( 𝑉 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
33 8 32 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
35 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ⊆ 𝑋 )
36 trnei ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
37 34 35 29 36 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
38 31 37 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
39 filfbas ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
40 38 39 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
41 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 : 𝐴 ⟶ 𝑌 )
42 fmval ⊢ ( ( 𝑌 ∈ V ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝑌 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝑌 filGen ran ( 𝑎 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑎 ) ) ) )
43 28 40 41 42 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝑌 filGen ran ( 𝑎 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑎 ) ) ) )
44 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑇 ∈ ( UnifOn ‘ 𝐴 ) )
45 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ( 𝑇 Cnu 𝑈 ) )
46 1 5 3 isusp ⊢ ( 𝑉 ∈ UnifSp ↔ ( 𝑆 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 = ( unifTop ‘ 𝑆 ) ) )
47 9 46 sylib ⊢ ( 𝜑 → ( 𝑆 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 = ( unifTop ‘ 𝑆 ) ) )
48 47 simpld ⊢ ( 𝜑 → 𝑆 ∈ ( UnifOn ‘ 𝑋 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ ( UnifOn ‘ 𝑋 ) )
50 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑉 ∈ UnifSp )
51 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑉 ∈ TopSp )
52 1 3 5 neipcfilu ⊢ ( ( 𝑉 ∈ UnifSp ∧ 𝑉 ∈ TopSp ∧ 𝑥 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ ( CauFilu ‘ 𝑆 ) )
53 50 51 29 52 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ ( CauFilu ‘ 𝑆 ) )
54 0nelfb ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) → ¬ ∅ ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) )
55 40 54 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ¬ ∅ ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) )
56 trcfilu ⊢ ( ( 𝑆 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ ( CauFilu ‘ 𝑆 ) ∧ ¬ ∅ ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( CauFilu ‘ ( 𝑆 ↾t ( 𝐴 × 𝐴 ) ) ) )
57 49 53 55 35 56 syl121anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( CauFilu ‘ ( 𝑆 ↾t ( 𝐴 × 𝐴 ) ) ) )
58 44 elfvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ V )
59 ressuss ⊢ ( 𝐴 ∈ V → ( UnifSt ‘ ( 𝑉 ↾s 𝐴 ) ) = ( ( UnifSt ‘ 𝑉 ) ↾t ( 𝐴 × 𝐴 ) ) )
60 5 oveq1i ⊢ ( 𝑆 ↾t ( 𝐴 × 𝐴 ) ) = ( ( UnifSt ‘ 𝑉 ) ↾t ( 𝐴 × 𝐴 ) )
61 59 6 60 3eqtr4g ⊢ ( 𝐴 ∈ V → 𝑇 = ( 𝑆 ↾t ( 𝐴 × 𝐴 ) ) )
62 61 fveq2d ⊢ ( 𝐴 ∈ V → ( CauFilu ‘ 𝑇 ) = ( CauFilu ‘ ( 𝑆 ↾t ( 𝐴 × 𝐴 ) ) ) )
63 58 62 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( CauFilu ‘ 𝑇 ) = ( CauFilu ‘ ( 𝑆 ↾t ( 𝐴 × 𝐴 ) ) ) )
64 57 63 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( CauFilu ‘ 𝑇 ) )
65 imaeq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑏 ) )
66 65 cbvmptv ⊢ ( 𝑎 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑎 ) ) = ( 𝑏 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑏 ) )
67 66 rneqi ⊢ ran ( 𝑎 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑎 ) ) = ran ( 𝑏 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑏 ) )
68 44 27 45 64 67 fmucnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ran ( 𝑎 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑎 ) ) ∈ ( CauFilu ‘ 𝑈 ) )
69 cfilufg ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑌 ) ∧ ran ( 𝑎 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑎 ) ) ∈ ( CauFilu ‘ 𝑈 ) ) → ( 𝑌 filGen ran ( 𝑎 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑎 ) ) ) ∈ ( CauFilu ‘ 𝑈 ) )
70 27 68 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑌 filGen ran ( 𝑎 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↦ ( 𝐹 “ 𝑎 ) ) ) ∈ ( CauFilu ‘ 𝑈 ) )
71 43 70 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( CauFilu ‘ 𝑈 ) )
72 1 2 3 4 7 8 10 11 12 13 26 15 71 cnextucn ⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )