Theorem cnextucn 24238

Description: Extension by continuity. Proposition 11 of [BourbakiTop1] p. II.20. Given a topology 𝐽 on 𝑋, a subset 𝐴 dense in 𝑋, this states a condition for 𝐹 from 𝐴 to a space 𝑌 Hausdorff and complete to be extensible by continuity. (Contributed by Thierry Arnoux, 4-Dec-2017.)

Hypotheses

Ref	Expression
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

Ref	Expression
cnextucn	⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐽   𝑥,𝐾   𝜑,𝑥

Allowed substitution hints:   𝑈(𝑥)   𝑉(𝑥)   𝑊(𝑥)   𝑋(𝑥)   𝑌(𝑥)

Proof of Theorem cnextucn

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098   ≠ wne 2930  Vcvv 3463   ⊆ wss 3945  ∅c0 4323  {csn 4629  ∪ cuni 4908  ⟶wf 6543  ‘cfv 6547  (class class class)co 7417  Basecbs 17179   ↾_t crest 17401  TopOpenctopn 17402  fBascfbas 21271  Topctop 22825  TopOnctopon 22842  TopSpctps 22864  clsccl 22952  neicnei 23031   Cn ccn 23158  Hauscha 23242  Regcreg 23243  Filcfil 23779   FilMap cfm 23867   fLim cflim 23868   fLimf cflf 23869  CnExtccnext 23993  UnifStcuss 24188  UnifSpcusp 24189  CauFil_uccfilu 24221  CUnifSpccusp 24232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-1st 7992  df-2nd 7993  df-1o 8485  df-er 8723  df-map 8845  df-pm 8846  df-en 8963  df-fin 8966  df-fi 9434  df-rest 17403  df-topgen 17424  df-fbas 21280  df-fg 21281  df-top 22826  df-topon 22843  df-topsp 22865  df-bases 22879  df-cld 22953  df-ntr 22954  df-cls 22955  df-nei 23032  df-cn 23161  df-cnp 23162  df-haus 23249  df-reg 23250  df-tx 23496  df-fil 23780  df-fm 23872  df-flim 23873  df-flf 23874  df-cnext 23994  df-ust 24135  df-utop 24166  df-usp 24192  df-cusp 24233

This theorem is referenced by:  ucnextcn  24239