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