Definition df-cnext 20433

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 20432	. 2 class CnExt
2		vj	. . 3 setvar j
3		vk	. . 3 setvar k
4		ctop 19267	. . 3 class Top
5		vf	. . . 4 setvar f
6	3	cv 1382	. . . . . 6 class k
7	6	cuni 4234	. . . . 5 class U. k
8	2	cv 1382	. . . . . 6 class j
9	8	cuni 4234	. . . . 5 class U. j
10		cpm 7423	. . . . 5 class ^pm
11	7, 9, 10	co 6281	. . . 4 class ( U. k ^pm U. j )
12		vx	. . . . 5 setvar x
13	5	cv 1382	. . . . . . 7 class f
14	13	cdm 4989	. . . . . 6 class dom f
15		ccl 19392	. . . . . . 7 class cls
16	8, 15	cfv 5578	. . . . . 6 class ( cls ` j )
17	14, 16	cfv 5578	. . . . 5 class ( ( cls ` j ) ` dom f )
18	12	cv 1382	. . . . . . 7 class x
19	18	csn 4014	. . . . . 6 class { x }
20		cnei 19471	. . . . . . . . . . 11 class nei
21	8, 20	cfv 5578	. . . . . . . . . 10 class ( nei ` j )
22	19, 21	cfv 5578	. . . . . . . . 9 class ( ( nei ` j ) ` { x } )
23		crest 14695	. . . . . . . . 9 class ↾t
24	22, 14, 23	co 6281	. . . . . . . 8 class ( ( ( nei ` j ) ` { x } ) ↾t dom f )
25		cflf 20309	. . . . . . . 8 class fLimf
26	6, 24, 25	co 6281	. . . . . . 7 class ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) )
27	13, 26	cfv 5578	. . . . . 6 class ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f )
28	19, 27	cxp 4987	. . . . 5 class ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f ) )
29	12, 17, 28	ciun 4315	. . . 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 4495	. . 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 6283	. 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 1383	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  20434