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

Definition df-concat 11426
Description: Define the concatenation operator which combines two words. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
df-concat  |- concat  =  ( s  e.  _V , 
t  e.  _V  |->  ( x  e.  ( 0..^ ( ( # `  s
)  +  ( # `  t ) ) ) 
|->  if ( x  e.  ( 0..^ ( # `  s ) ) ,  ( s `  x
) ,  ( t `
 ( x  -  ( # `  s ) ) ) ) ) )
Distinct variable group:    t, s, x

Detailed syntax breakdown of Definition df-concat
StepHypRef Expression
1 cconcat 11420 . 2  class concat
2 vs . . 3  set  s
3 vt . . 3  set  t
4 cvv 2801 . . 3  class  _V
5 vx . . . 4  set  x
6 cc0 8753 . . . . 5  class  0
72cv 1631 . . . . . . 7  class  s
8 chash 11353 . . . . . . 7  class  #
97, 8cfv 5271 . . . . . 6  class  ( # `  s )
103cv 1631 . . . . . . 7  class  t
1110, 8cfv 5271 . . . . . 6  class  ( # `  t )
12 caddc 8756 . . . . . 6  class  +
139, 11, 12co 5874 . . . . 5  class  ( (
# `  s )  +  ( # `  t
) )
14 cfzo 10886 . . . . 5  class ..^
156, 13, 14co 5874 . . . 4  class  ( 0..^ ( ( # `  s
)  +  ( # `  t ) ) )
165cv 1631 . . . . . 6  class  x
176, 9, 14co 5874 . . . . . 6  class  ( 0..^ ( # `  s
) )
1816, 17wcel 1696 . . . . 5  wff  x  e.  ( 0..^ ( # `  s ) )
1916, 7cfv 5271 . . . . 5  class  ( s `
 x )
20 cmin 9053 . . . . . . 7  class  -
2116, 9, 20co 5874 . . . . . 6  class  ( x  -  ( # `  s
) )
2221, 10cfv 5271 . . . . 5  class  ( t `
 ( x  -  ( # `  s ) ) )
2318, 19, 22cif 3578 . . . 4  class  if ( x  e.  ( 0..^ ( # `  s
) ) ,  ( s `  x ) ,  ( t `  ( x  -  ( # `
 s ) ) ) )
245, 15, 23cmpt 4093 . . 3  class  ( x  e.  ( 0..^ ( ( # `  s
)  +  ( # `  t ) ) ) 
|->  if ( x  e.  ( 0..^ ( # `  s ) ) ,  ( s `  x
) ,  ( t `
 ( x  -  ( # `  s ) ) ) ) )
252, 3, 4, 4, 24cmpt2 5876 . 2  class  ( s  e.  _V ,  t  e.  _V  |->  ( x  e.  ( 0..^ ( ( # `  s
)  +  ( # `  t ) ) ) 
|->  if ( x  e.  ( 0..^ ( # `  s ) ) ,  ( s `  x
) ,  ( t `
 ( x  -  ( # `  s ) ) ) ) ) )
261, 25wceq 1632 1  wff concat  =  ( s  e.  _V , 
t  e.  _V  |->  ( x  e.  ( 0..^ ( ( # `  s
)  +  ( # `  t ) ) ) 
|->  if ( x  e.  ( 0..^ ( # `  s ) ) ,  ( s `  x
) ,  ( t `
 ( x  -  ( # `  s ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  ccatfn  11443  ccatfval  11444
  Copyright terms: Public domain W3C validator