Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-conc Unicode version

Definition df-conc 26108
Description: Concatenation of two words. Experimental. (Contributed by FL, 14-Jan-2014.)
Assertion
Ref Expression
df-conc  |-  conc  =  ( x  e.  _V ,  y  e.  _V  |->  if ( x  =  (/) ,  y ,  if ( y  =  (/) ,  x ,  ( x  u.  ( a  e.  ( ( ( # `  x
)  +  1 ) ... ( ( # `  x )  +  (
# `  y )
) )  |->  ( y `
 ( a  -  ( # `  x ) ) ) ) ) ) ) )
Distinct variable group:    x, y, a

Detailed syntax breakdown of Definition df-conc
StepHypRef Expression
1 cconc 26107 . 2  class  conc
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cvv 2801 . . 3  class  _V
52cv 1631 . . . . 5  class  x
6 c0 3468 . . . . 5  class  (/)
75, 6wceq 1632 . . . 4  wff  x  =  (/)
83cv 1631 . . . 4  class  y
98, 6wceq 1632 . . . . 5  wff  y  =  (/)
10 va . . . . . . 7  set  a
11 chash 11353 . . . . . . . . . 10  class  #
125, 11cfv 5271 . . . . . . . . 9  class  ( # `  x )
13 c1 8754 . . . . . . . . 9  class  1
14 caddc 8756 . . . . . . . . 9  class  +
1512, 13, 14co 5874 . . . . . . . 8  class  ( (
# `  x )  +  1 )
168, 11cfv 5271 . . . . . . . . 9  class  ( # `  y )
1712, 16, 14co 5874 . . . . . . . 8  class  ( (
# `  x )  +  ( # `  y
) )
18 cfz 10798 . . . . . . . 8  class  ...
1915, 17, 18co 5874 . . . . . . 7  class  ( ( ( # `  x
)  +  1 ) ... ( ( # `  x )  +  (
# `  y )
) )
2010cv 1631 . . . . . . . . 9  class  a
21 cmin 9053 . . . . . . . . 9  class  -
2220, 12, 21co 5874 . . . . . . . 8  class  ( a  -  ( # `  x
) )
2322, 8cfv 5271 . . . . . . 7  class  ( y `
 ( a  -  ( # `  x ) ) )
2410, 19, 23cmpt 4093 . . . . . 6  class  ( a  e.  ( ( (
# `  x )  +  1 ) ... ( ( # `  x
)  +  ( # `  y ) ) ) 
|->  ( y `  (
a  -  ( # `  x ) ) ) )
255, 24cun 3163 . . . . 5  class  ( x  u.  ( a  e.  ( ( ( # `  x )  +  1 ) ... ( (
# `  x )  +  ( # `  y
) ) )  |->  ( y `  ( a  -  ( # `  x
) ) ) ) )
269, 5, 25cif 3578 . . . 4  class  if ( y  =  (/) ,  x ,  ( x  u.  ( a  e.  ( ( ( # `  x
)  +  1 ) ... ( ( # `  x )  +  (
# `  y )
) )  |->  ( y `
 ( a  -  ( # `  x ) ) ) ) ) )
277, 8, 26cif 3578 . . 3  class  if ( x  =  (/) ,  y ,  if ( y  =  (/) ,  x ,  ( x  u.  (
a  e.  ( ( ( # `  x
)  +  1 ) ... ( ( # `  x )  +  (
# `  y )
) )  |->  ( y `
 ( a  -  ( # `  x ) ) ) ) ) ) )
282, 3, 4, 4, 27cmpt2 5876 . 2  class  ( x  e.  _V ,  y  e.  _V  |->  if ( x  =  (/) ,  y ,  if ( y  =  (/) ,  x ,  ( x  u.  (
a  e.  ( ( ( # `  x
)  +  1 ) ... ( ( # `  x )  +  (
# `  y )
) )  |->  ( y `
 ( a  -  ( # `  x ) ) ) ) ) ) ) )
291, 28wceq 1632 1  wff  conc  =  ( x  e.  _V ,  y  e.  _V  |->  if ( x  =  (/) ,  y ,  if ( y  =  (/) ,  x ,  ( x  u.  ( a  e.  ( ( ( # `  x
)  +  1 ) ... ( ( # `  x )  +  (
# `  y )
) )  |->  ( y `
 ( a  -  ( # `  x ) ) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  isconc1  26109  isconc2  26110  isconc3  26111
  Copyright terms: Public domain W3C validator