This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )