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	|- X = ( Base ` V )
	ucnextcn.y	|- Y = ( Base ` W )
	ucnextcn.j	|- J = ( TopOpen ` V )
	ucnextcn.k	|- K = ( TopOpen ` W )
	ucnextcn.s	|- S = ( UnifSt ` V )
	ucnextcn.t	|- T = ( UnifSt ` ( V |`s A ) )
	ucnextcn.u	|- U = ( UnifSt ` W )
	ucnextcn.v	|- ( ph -> V e. TopSp )
	ucnextcn.r	|- ( ph -> V e. UnifSp )
	ucnextcn.w	|- ( ph -> W e. TopSp )
	ucnextcn.z	|- ( ph -> W e. CUnifSp )
	ucnextcn.h	|- ( ph -> K e. Haus )
	ucnextcn.a	|- ( ph -> A C_ X )
	ucnextcn.f	|- ( ph -> F e. ( T uCn U ) )
	ucnextcn.c	|- ( ph -> ( ( cls ` J ) ` A ) = X )
Assertion	ucnextcn	|- ( ph -> ( ( J CnExt K ) ` F ) e. ( J Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		ucnextcn.x	|- X = ( Base ` V )
2		ucnextcn.y	|- Y = ( Base ` W )
3		ucnextcn.j	|- J = ( TopOpen ` V )
4		ucnextcn.k	|- K = ( TopOpen ` W )
5		ucnextcn.s	|- S = ( UnifSt ` V )
6		ucnextcn.t	|- T = ( UnifSt ` ( V |`s A ) )
7		ucnextcn.u	|- U = ( UnifSt ` W )
8		ucnextcn.v	|- ( ph -> V e. TopSp )
9		ucnextcn.r	|- ( ph -> V e. UnifSp )
10		ucnextcn.w	|- ( ph -> W e. TopSp )
11		ucnextcn.z	|- ( ph -> W e. CUnifSp )
12		ucnextcn.h	|- ( ph -> K e. Haus )
13		ucnextcn.a	|- ( ph -> A C_ X )
14		ucnextcn.f	|- ( ph -> F e. ( T uCn U ) )
15		ucnextcn.c	|- ( ph -> ( ( cls ` J ) ` A ) = X )
16	1 6	ressust	|- ( ( V e. UnifSp /\ A C_ X ) -> T e. ( UnifOn ` A ) )
17	9 13 16	syl2anc	|- ( ph -> T e. ( UnifOn ` A ) )
18		cuspusp	|- ( W e. CUnifSp -> W e. UnifSp )
19	11 18	syl	|- ( ph -> W e. UnifSp )
20	2 7 4	isusp	|- ( W e. UnifSp <-> ( U e. ( UnifOn ` Y ) /\ K = ( unifTop ` U ) ) )
21	19 20	sylib	|- ( ph -> ( U e. ( UnifOn ` Y ) /\ K = ( unifTop ` U ) ) )
22	21	simpld	|- ( ph -> U e. ( UnifOn ` Y ) )
23		isucn	|- ( ( T e. ( UnifOn ` A ) /\ U e. ( UnifOn ` Y ) ) -> ( F e. ( T uCn U ) <-> ( F : A --> Y /\ A. w e. U E. v e. T A. y e. A A. z e. A ( y v z -> ( F ` y ) w ( F ` z ) ) ) ) )
24	17 22 23	syl2anc	|- ( ph -> ( F e. ( T uCn U ) <-> ( F : A --> Y /\ A. w e. U E. v e. T A. y e. A A. z e. A ( y v z -> ( F ` y ) w ( F ` z ) ) ) ) )
25	14 24	mpbid	|- ( ph -> ( F : A --> Y /\ A. w e. U E. v e. T A. y e. A A. z e. A ( y v z -> ( F ` y ) w ( F ` z ) ) ) )
26	25	simpld	|- ( ph -> F : A --> Y )
27	22	adantr	|- ( ( ph /\ x e. X ) -> U e. ( UnifOn ` Y ) )
28	27	elfvexd	|- ( ( ph /\ x e. X ) -> Y e. _V )
29		simpr	|- ( ( ph /\ x e. X ) -> x e. X )
30	15	adantr	|- ( ( ph /\ x e. X ) -> ( ( cls ` J ) ` A ) = X )
31	29 30	eleqtrrd	|- ( ( ph /\ x e. X ) -> x e. ( ( cls ` J ) ` A ) )
32	1 3	istps	|- ( V e. TopSp <-> J e. ( TopOn ` X ) )
33	8 32	sylib	|- ( ph -> J e. ( TopOn ` X ) )
34	33	adantr	|- ( ( ph /\ x e. X ) -> J e. ( TopOn ` X ) )
35	13	adantr	|- ( ( ph /\ x e. X ) -> A C_ X )
36		trnei	|- ( ( J e. ( TopOn ` X ) /\ A C_ X /\ x e. X ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) )
37	34 35 29 36	syl3anc	|- ( ( ph /\ x e. X ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) )
38	31 37	mpbid	|- ( ( ph /\ x e. X ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) )
39		filfbas	|- ( ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( fBas ` A ) )
40	38 39	syl	|- ( ( ph /\ x e. X ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( fBas ` A ) )
41	26	adantr	|- ( ( ph /\ x e. X ) -> F : A --> Y )
42		fmval	|- ( ( Y e. _V /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( fBas ` A ) /\ F : A --> Y ) -> ( ( Y FilMap F ) ` ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( Y filGen ran ( a e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " a ) ) ) )
43	28 40 41 42	syl3anc	|- ( ( ph /\ x e. X ) -> ( ( Y FilMap F ) ` ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( Y filGen ran ( a e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " a ) ) ) )
44	17	adantr	|- ( ( ph /\ x e. X ) -> T e. ( UnifOn ` A ) )
45	14	adantr	|- ( ( ph /\ x e. X ) -> F e. ( T uCn U ) )
46	1 5 3	isusp	|- ( V e. UnifSp <-> ( S e. ( UnifOn ` X ) /\ J = ( unifTop ` S ) ) )
47	9 46	sylib	|- ( ph -> ( S e. ( UnifOn ` X ) /\ J = ( unifTop ` S ) ) )
48	47	simpld	|- ( ph -> S e. ( UnifOn ` X ) )
49	48	adantr	|- ( ( ph /\ x e. X ) -> S e. ( UnifOn ` X ) )
50	9	adantr	|- ( ( ph /\ x e. X ) -> V e. UnifSp )
51	8	adantr	|- ( ( ph /\ x e. X ) -> V e. TopSp )
52	1 3 5	neipcfilu	|- ( ( V e. UnifSp /\ V e. TopSp /\ x e. X ) -> ( ( nei ` J ) ` { x } ) e. ( CauFilU ` S ) )
53	50 51 29 52	syl3anc	|- ( ( ph /\ x e. X ) -> ( ( nei ` J ) ` { x } ) e. ( CauFilU ` S ) )
54		0nelfb	|- ( ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( fBas ` A ) -> -. (/) e. ( ( ( nei ` J ) ` { x } ) |`t A ) )
55	40 54	syl	|- ( ( ph /\ x e. X ) -> -. (/) e. ( ( ( nei ` J ) ` { x } ) |`t A ) )
56		trcfilu	|- ( ( S e. ( UnifOn ` X ) /\ ( ( ( nei ` J ) ` { x } ) e. ( CauFilU ` S ) /\ -. (/) e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) /\ A C_ X ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( CauFilU ` ( S |`t ( A X. A ) ) ) )
57	49 53 55 35 56	syl121anc	|- ( ( ph /\ x e. X ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( CauFilU ` ( S |`t ( A X. A ) ) ) )
58	44	elfvexd	|- ( ( ph /\ x e. X ) -> A e. _V )
59		ressuss	|- ( A e. _V -> ( UnifSt ` ( V |`s A ) ) = ( ( UnifSt ` V ) |`t ( A X. A ) ) )
60	5	oveq1i	|- ( S |`t ( A X. A ) ) = ( ( UnifSt ` V ) |`t ( A X. A ) )
61	59 6 60	3eqtr4g	|- ( A e. _V -> T = ( S |`t ( A X. A ) ) )
62	61	fveq2d	|- ( A e. _V -> ( CauFilU ` T ) = ( CauFilU ` ( S |`t ( A X. A ) ) ) )
63	58 62	syl	|- ( ( ph /\ x e. X ) -> ( CauFilU ` T ) = ( CauFilU ` ( S |`t ( A X. A ) ) ) )
64	57 63	eleqtrrd	|- ( ( ph /\ x e. X ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( CauFilU ` T ) )
65		imaeq2	|- ( a = b -> ( F " a ) = ( F " b ) )
66	65	cbvmptv	|- ( a e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " a ) ) = ( b e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " b ) )
67	66	rneqi	|- ran ( a e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " a ) ) = ran ( b e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " b ) )
68	44 27 45 64 67	fmucnd	|- ( ( ph /\ x e. X ) -> ran ( a e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " a ) ) e. ( CauFilU ` U ) )
69		cfilufg	|- ( ( U e. ( UnifOn ` Y ) /\ ran ( a e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " a ) ) e. ( CauFilU ` U ) ) -> ( Y filGen ran ( a e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " a ) ) ) e. ( CauFilU ` U ) )
70	27 68 69	syl2anc	|- ( ( ph /\ x e. X ) -> ( Y filGen ran ( a e. ( ( ( nei ` J ) ` { x } ) |`t A ) |-> ( F " a ) ) ) e. ( CauFilU ` U ) )
71	43 70	eqeltrd	|- ( ( ph /\ x e. X ) -> ( ( Y FilMap F ) ` ( ( ( nei ` J ) ` { x } ) |`t A ) ) e. ( CauFilU ` U ) )
72	1 2 3 4 7 8 10 11 12 13 26 15 71	cnextucn	|- ( ph -> ( ( J CnExt K ) ` F ) e. ( J Cn K ) )