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 ⊢ 𝑋 = ( Base ‘ 𝑉 )
cnextucn.y ⊢ 𝑌 = ( Base ‘ 𝑊 )
cnextucn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑉 )
cnextucn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑊 )
cnextucn.u ⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
cnextucn.v ⊢ ( 𝜑 → 𝑉 ∈ TopSp )
cnextucn.t ⊢ ( 𝜑 → 𝑊 ∈ TopSp )
cnextucn.w ⊢ ( 𝜑 → 𝑊 ∈ CUnifSp )
cnextucn.h ⊢ ( 𝜑 → 𝐾 ∈ Haus )
cnextucn.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
cnextucn.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑌 )
cnextucn.c ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
cnextucn.l ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( CauFilu ‘ 𝑈 ) )
Assertion cnextucn ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cnextucn.x ⊢ 𝑋 = ( Base ‘ 𝑉 )
2 cnextucn.y ⊢ 𝑌 = ( Base ‘ 𝑊 )
3 cnextucn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑉 )
4 cnextucn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑊 )
5 cnextucn.u ⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
6 cnextucn.v ⊢ ( 𝜑 → 𝑉 ∈ TopSp )
7 cnextucn.t ⊢ ( 𝜑 → 𝑊 ∈ TopSp )
8 cnextucn.w ⊢ ( 𝜑 → 𝑊 ∈ CUnifSp )
9 cnextucn.h ⊢ ( 𝜑 → 𝐾 ∈ Haus )
10 cnextucn.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
11 cnextucn.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑌 )
12 cnextucn.c ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
13 cnextucn.l ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( CauFilu ‘ 𝑈 ) )
14 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
15 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
16 3 tpstop ⊢ ( 𝑉 ∈ TopSp → 𝐽 ∈ Top )
17 6 16 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
18 2 4 tpsuni ⊢ ( 𝑊 ∈ TopSp → 𝑌 = ∪ 𝐾 )
19 7 18 syl ⊢ ( 𝜑 → 𝑌 = ∪ 𝐾 )
20 19 feq3d ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝑌 ↔ 𝐹 : 𝐴 ⟶ ∪ 𝐾 ) )
21 11 20 mpbid ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ∪ 𝐾 )
22 1 3 tpsuni ⊢ ( 𝑉 ∈ TopSp → 𝑋 = ∪ 𝐽 )
23 6 22 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
24 10 23 sseqtrd ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐽 )
25 12 23 eqtrd ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ∪ 𝐽 )
26 2 4 istps ⊢ ( 𝑊 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
27 7 26 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
29 23 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝐽 ) )
30 29 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝑥 ∈ 𝑋 )
31 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
32 30 31 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
33 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
34 17 33 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
35 fveq2 ⊢ ( 𝑋 = ∪ 𝐽 → ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ∪ 𝐽 ) )
36 35 eleq2d ⊢ ( 𝑋 = ∪ 𝐽 → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) )
37 23 36 syl ⊢ ( 𝜑 → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) )
38 34 37 mpbird ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
40 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐴 ⊆ 𝑋 )
41 trnei ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
42 39 40 30 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
43 32 42 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
44 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐹 : 𝐴 ⟶ 𝑌 )
45 flfval ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝑌 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ) )
46 28 43 44 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ) )
47 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝑊 ∈ CUnifSp )
48 30 13 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( CauFilu ‘ 𝑈 ) )
49 5 fveq2i ⊢ ( CauFilu ‘ 𝑈 ) = ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) )
50 48 49 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) )
51 2 fvexi ⊢ 𝑌 ∈ V
52 filfbas ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
53 43 52 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
54 fmfil ⊢ ( ( 𝑌 ∈ V ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝑌 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( Fil ‘ 𝑌 ) )
55 51 53 44 54 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( Fil ‘ 𝑌 ) )
56 2 4 cuspcvg ⊢ ( ( 𝑊 ∈ CUnifSp ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ) ≠ ∅ )
57 47 50 55 56 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ) ≠ ∅ )
58 46 57 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
59 cuspusp ⊢ ( 𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp )
60 8 59 syl ⊢ ( 𝜑 → 𝑊 ∈ UnifSp )
61 4 uspreg ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝐾 ∈ Haus ) → 𝐾 ∈ Reg )
62 60 9 61 syl2anc ⊢ ( 𝜑 → 𝐾 ∈ Reg )
63 14 15 17 9 21 24 25 58 62 cnextcn ⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )