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

Definition df-dwords 26088
Description: Words of size S over an alphabet  A with all the elements different. (For my private use only. Don't use.) (Contributed by FL, 26-May-2016.)
Assertion
Ref Expression
df-dwords  |- dWords  =  ( a  e.  _V , 
s  e.  NN0  |->  { w  e.  ( a  Words  s )  |  A. x  e.  ( 1 ... s
) A. y  e.  ( 1 ... s
) ( x  =/=  y  ->  ( w `  x )  =/=  (
w `  y )
) } )
Distinct variable group:    s, a, w, x, y

Detailed syntax breakdown of Definition df-dwords
StepHypRef Expression
1 cdwords 26087 . 2  class dWords
2 va . . 3  set  a
3 vs . . 3  set  s
4 cvv 2801 . . 3  class  _V
5 cn0 9981 . . 3  class  NN0
6 vx . . . . . . . . 9  set  x
76cv 1631 . . . . . . . 8  class  x
8 vy . . . . . . . . 9  set  y
98cv 1631 . . . . . . . 8  class  y
107, 9wne 2459 . . . . . . 7  wff  x  =/=  y
11 vw . . . . . . . . . 10  set  w
1211cv 1631 . . . . . . . . 9  class  w
137, 12cfv 5271 . . . . . . . 8  class  ( w `
 x )
149, 12cfv 5271 . . . . . . . 8  class  ( w `
 y )
1513, 14wne 2459 . . . . . . 7  wff  ( w `
 x )  =/=  ( w `  y
)
1610, 15wi 4 . . . . . 6  wff  ( x  =/=  y  ->  (
w `  x )  =/=  ( w `  y
) )
17 c1 8754 . . . . . . 7  class  1
183cv 1631 . . . . . . 7  class  s
19 cfz 10798 . . . . . . 7  class  ...
2017, 18, 19co 5874 . . . . . 6  class  ( 1 ... s )
2116, 8, 20wral 2556 . . . . 5  wff  A. y  e.  ( 1 ... s
) ( x  =/=  y  ->  ( w `  x )  =/=  (
w `  y )
)
2221, 6, 20wral 2556 . . . 4  wff  A. x  e.  ( 1 ... s
) A. y  e.  ( 1 ... s
) ( x  =/=  y  ->  ( w `  x )  =/=  (
w `  y )
)
232cv 1631 . . . . 5  class  a
24 cwrd 26084 . . . . 5  class  Words
2523, 18, 24co 5874 . . . 4  class  ( a 
Words  s )
2622, 11, 25crab 2560 . . 3  class  { w  e.  ( a  Words  s )  |  A. x  e.  ( 1 ... s
) A. y  e.  ( 1 ... s
) ( x  =/=  y  ->  ( w `  x )  =/=  (
w `  y )
) }
272, 3, 4, 5, 26cmpt2 5876 . 2  class  ( a  e.  _V ,  s  e.  NN0  |->  { w  e.  ( a  Words  s )  |  A. x  e.  ( 1 ... s
) A. y  e.  ( 1 ... s
) ( x  =/=  y  ->  ( w `  x )  =/=  (
w `  y )
) } )
281, 27wceq 1632 1  wff dWords  =  ( a  e.  _V , 
s  e.  NN0  |->  { w  e.  ( a  Words  s )  |  A. x  e.  ( 1 ... s
) A. y  e.  ( 1 ... s
) ( x  =/=  y  ->  ( w `  x )  =/=  (
w `  y )
) } )
Colors of variables: wff set class
This definition is referenced by:  isnword  26089
  Copyright terms: Public domain W3C validator