MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnext Structured version   Unicode version

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
StepHypRef 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
63cv 1369 . . . . . 6  class  k
76cuni 4202 . . . . 5  class  U. k
82cv 1369 . . . . . 6  class  j
98cuni 4202 . . . . 5  class  U. j
10 cpm 7328 . . . . 5  class  ^pm
117, 9, 10co 6203 . . . 4  class  ( U. k  ^pm  U. j )
12 vx . . . . 5  setvar  x
135cv 1369 . . . . . . 7  class  f
1413cdm 4951 . . . . . 6  class  dom  f
15 ccl 18764 . . . . . . 7  class  cls
168, 15cfv 5529 . . . . . 6  class  ( cls `  j )
1714, 16cfv 5529 . . . . 5  class  ( ( cls `  j ) `
 dom  f )
1812cv 1369 . . . . . . 7  class  x
1918csn 3988 . . . . . 6  class  { x }
20 cnei 18843 . . . . . . . . . . 11  class  nei
218, 20cfv 5529 . . . . . . . . . 10  class  ( nei `  j )
2219, 21cfv 5529 . . . . . . . . 9  class  ( ( nei `  j ) `
 { x }
)
23 crest 14482 . . . . . . . . 9  classt
2422, 14, 23co 6203 . . . . . . . 8  class  ( ( ( nei `  j
) `  { x } )t  dom  f )
25 cflf 19650 . . . . . . . 8  class  fLimf
266, 24, 25co 6203 . . . . . . 7  class  ( k 
fLimf  ( ( ( nei `  j ) `  {
x } )t  dom  f
) )
2713, 26cfv 5529 . . . . . 6  class  ( ( k  fLimf  ( (
( nei `  j
) `  { x } )t  dom  f ) ) `
 f )
2819, 27cxp 4949 . . . . 5  class  ( { x }  X.  (
( k  fLimf  ( ( ( nei `  j
) `  { x } )t  dom  f ) ) `
 f ) )
2912, 17, 28ciun 4282 . . . 4  class  U_ x  e.  ( ( cls `  j
) `  dom  f ) ( { x }  X.  ( ( k  fLimf  ( ( ( nei `  j
) `  { x } )t  dom  f ) ) `
 f ) )
305, 11, 29cmpt 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 ) ) )
312, 3, 4, 4, 30cmpt2 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 ) ) ) )
321, 31wceq 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 ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  cnextval  19775
  Copyright terms: Public domain W3C validator