Definition df-cnext 19774

Description: Define the continuous extension of a given function. (Contributed by Thierry Arnoux, 1-Dec-2017.)

Assertion

Ref	Expression
df-cnext	|- CnExt = ( j e. Top , k e. Top |-> ( f e. ( U. k ^pm U. j ) |-> U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f ) ) ) )

Distinct variable group:   j, k, f, x

Detailed syntax breakdown of Definition df-cnext

Step	Hyp	Ref	Expression
1		ccnext 19773	. 2 class CnExt
2		vj	. . 3 setvar j
3		vk	. . 3 setvar k
4		ctop 18640	. . 3 class Top
5		vf	. . . 4 setvar f
6	3	cv 1369	. . . . . 6 class k
7	6	cuni 4202	. . . . 5 class U. k
8	2	cv 1369	. . . . . 6 class j
9	8	cuni 4202	. . . . 5 class U. j
10		cpm 7328	. . . . 5 class ^pm
11	7, 9, 10	co 6203	. . . 4 class ( U. k ^pm U. j )
12		vx	. . . . 5 setvar x
13	5	cv 1369	. . . . . . 7 class f
14	13	cdm 4951	. . . . . 6 class dom f
15		ccl 18764	. . . . . . 7 class cls
16	8, 15	cfv 5529	. . . . . 6 class ( cls ` j )
17	14, 16	cfv 5529	. . . . 5 class ( ( cls ` j ) ` dom f )
18	12	cv 1369	. . . . . . 7 class x
19	18	csn 3988	. . . . . 6 class { x }
20		cnei 18843	. . . . . . . . . . 11 class nei
21	8, 20	cfv 5529	. . . . . . . . . 10 class ( nei ` j )
22	19, 21	cfv 5529	. . . . . . . . 9 class ( ( nei ` j ) ` { x } )
23		crest 14482	. . . . . . . . 9 class ↾t
24	22, 14, 23	co 6203	. . . . . . . 8 class ( ( ( nei ` j ) ` { x } ) ↾t dom f )
25		cflf 19650	. . . . . . . 8 class fLimf
26	6, 24, 25	co 6203	. . . . . . 7 class ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) )
27	13, 26	cfv 5529	. . . . . 6 class ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f )
28	19, 27	cxp 4949	. . . . 5 class ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f ) )
29	12, 17, 28	ciun 4282	. . . 4 class U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f ) )
30	5, 11, 29	cmpt 4461	. . 3 class ( f e. ( U. k ^pm U. j ) |-> U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f ) ) )
31	2, 3, 4, 4, 30	cmpt2 6205	. 2 class ( j e. Top , k e. Top |-> ( f e. ( U. k ^pm U. j ) |-> U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f ) ) ) )
32	1, 31	wceq 1370	1 wff CnExt = ( j e. Top , k e. Top |-> ( f e. ( U. k ^pm U. j ) |-> U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f ) ) ) )

This definition is referenced by:  cnextval  19775