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

Definition df-concat 11410
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 11404 . 2  class concat
2 vs . . 3  set  s
3 vt . . 3  set  t
4 cvv 2788 . . 3  class  _V
5 vx . . . 4  set  x
6 cc0 8737 . . . . 5  class  0
72cv 1622 . . . . . . 7  class  s
8 chash 11337 . . . . . . 7  class  #
97, 8cfv 5255 . . . . . 6  class  ( # `  s )
103cv 1622 . . . . . . 7  class  t
1110, 8cfv 5255 . . . . . 6  class  ( # `  t )
12 caddc 8740 . . . . . 6  class  +
139, 11, 12co 5858 . . . . 5  class  ( (
# `  s )  +  ( # `  t
) )
14 cfzo 10870 . . . . 5  class ..^
156, 13, 14co 5858 . . . 4  class  ( 0..^ ( ( # `  s
)  +  ( # `  t ) ) )
165cv 1622 . . . . . 6  class  x
176, 9, 14co 5858 . . . . . 6  class  ( 0..^ ( # `  s
) )
1816, 17wcel 1684 . . . . 5  wff  x  e.  ( 0..^ ( # `  s ) )
1916, 7cfv 5255 . . . . 5  class  ( s `
 x )
20 cmin 9037 . . . . . . 7  class  -
2116, 9, 20co 5858 . . . . . 6  class  ( x  -  ( # `  s
) )
2221, 10cfv 5255 . . . . 5  class  ( t `
 ( x  -  ( # `  s ) ) )
2318, 19, 22cif 3565 . . . 4  class  if ( x  e.  ( 0..^ ( # `  s
) ) ,  ( s `  x ) ,  ( t `  ( x  -  ( # `
 s ) ) ) )
245, 15, 23cmpt 4077 . . 3  class  ( x  e.  ( 0..^ ( ( # `  s
)  +  ( # `  t ) ) ) 
|->  if ( x  e.  ( 0..^ ( # `  s ) ) ,  ( s `  x
) ,  ( t `
 ( x  -  ( # `  s ) ) ) ) )
252, 3, 4, 4, 24cmpt2 5860 . 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 1623 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  11427  ccatfval  11428
  Copyright terms: Public domain W3C validator