Metamath Proof Explorer

Definition df-hash

Description: Define the set size function # , which gives the cardinality of a finite set as a member of NN0 , and assigns all infinite sets the value +oo . For example, ( #{ 0 , 1 , 2 } ) = 3 ( ex-hash ). (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion df-hash 
|- # = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chash 
 |-  #
1 vx 
 |-  x
2 cvv 
 |-  _V
3 1 cv 
 |-  x
4 caddc 
 |-  +
5 c1 
 |-  1
6 3 5 4 co 
 |-  ( x + 1 )
7 1 2 6 cmpt 
 |-  ( x e. _V |-> ( x + 1 ) )
8 cc0 
 |-  0
9 7 8 crdg 
 |-  rec ( ( x e. _V |-> ( x + 1 ) ) , 0 )
10 com 
 |-  _om
11 9 10 cres 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
12 ccrd 
 |-  card
13 11 12 ccom 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
14 cfn 
 |-  Fin
15 2 14 cdif 
 |-  ( _V \ Fin )
16 cpnf 
 |-  +oo
17 16 csn 
 |-  { +oo }
18 15 17 cxp 
 |-  ( ( _V \ Fin ) X. { +oo } )
19 13 18 cun 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )
20 0 19 wceq 
 |-  # = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )