Definition df-cnext

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnext	|- CnExt
1		vj	|- j
2		ctop	|- Top
3		vk	|- k
4		vf	|- f
5	3	cv	|- k
6	5	cuni	|- U. k
7		cpm	|- ^pm
8	1	cv	|- j
9	8	cuni	|- U. j
10	6 9 7	co	|- ( U. k ^pm U. j )
11		vx	|- x
12		ccl	|- cls
13	8 12	cfv	|- ( cls ` j )
14	4	cv	|- f
15	14	cdm	|- dom f
16	15 13	cfv	|- ( ( cls ` j ) ` dom f )
17	11	cv	|- x
18	17	csn	|- { x }
19		cflf	|- fLimf
20		cnei	|- nei
21	8 20	cfv	|- ( nei ` j )
22	18 21	cfv	|- ( ( nei ` j ) ` { x } )
23		crest	|- |`t
24	22 15 23	co	|- ( ( ( nei ` j ) ` { x } ) |`t dom f )
25	5 24 19	co	|- ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) )
26	14 25	cfv	|- ( ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) ` f )
27	18 26	cxp	|- ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) ` f ) )
28	11 16 27	ciun	|- U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) ` f ) )
29	4 10 28	cmpt	|- ( 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 ) ) )
30	1 3 2 2 29	cmpo	|- ( 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 ) ) ) )
31	0 30	wceq	|- 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 ) ) ) )