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

Definition df-hash 11338
Description: Define the  # function, which gives the cardinality of a finite set as a member of  NN0, and assigns all infinite sets the value  +oo. (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
df-hash  |-  #  =  ( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om )  o.  card )  u.  (
( _V  \  Fin )  X.  {  +oo }
) )

Detailed syntax breakdown of Definition df-hash
StepHypRef Expression
1 chash 11337 . 2  class  #
2 vx . . . . . . 7  set  x
3 cvv 2788 . . . . . . 7  class  _V
42cv 1622 . . . . . . . 8  class  x
5 c1 8738 . . . . . . . 8  class  1
6 caddc 8740 . . . . . . . 8  class  +
74, 5, 6co 5858 . . . . . . 7  class  ( x  +  1 )
82, 3, 7cmpt 4077 . . . . . 6  class  ( x  e.  _V  |->  ( x  +  1 ) )
9 cc0 8737 . . . . . 6  class  0
108, 9crdg 6422 . . . . 5  class  rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )
11 com 4656 . . . . 5  class  om
1210, 11cres 4691 . . . 4  class  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om )
13 ccrd 7568 . . . 4  class  card
1412, 13ccom 4693 . . 3  class  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om )  o.  card )
15 cfn 6863 . . . . 5  class  Fin
163, 15cdif 3149 . . . 4  class  ( _V 
\  Fin )
17 cpnf 8864 . . . . 5  class  +oo
1817csn 3640 . . . 4  class  {  +oo }
1916, 18cxp 4687 . . 3  class  ( ( _V  \  Fin )  X.  {  +oo } )
2014, 19cun 3150 . 2  class  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om )  o.  card )  u.  ( ( _V  \  Fin )  X. 
{  +oo } ) )
211, 20wceq 1623 1  wff  #  =  ( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om )  o.  card )  u.  (
( _V  \  Fin )  X.  {  +oo }
) )
Colors of variables: wff set class
This definition is referenced by:  hashgval  11340  hashinf  11342  hashf  11344
  Copyright terms: Public domain W3C validator