Definition df-hash 13118

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 27310). (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

Step	Hyp	Ref	Expression
1		chash 13117	. 2 class #
2		vx	. . . . . . 7 setvar x
3		cvv 3200	. . . . . . 7 class _V
4	2	cv 1482	. . . . . . . 8 class x
5		c1 9937	. . . . . . . 8 class 1
6		caddc 9939	. . . . . . . 8 class +
7	4, 5, 6	co 6650	. . . . . . 7 class ( x + 1 )
8	2, 3, 7	cmpt 4729	. . . . . 6 class ( x e. _V |-> ( x + 1 ) )
9		cc0 9936	. . . . . 6 class 0
10	8, 9	crdg 7505	. . . . 5 class rec ( ( x e. _V |-> ( x + 1 ) ) , 0 )
11		com 7065	. . . . 5 class om
12	10, 11	cres 5116	. . . 4 class ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` om )
13		ccrd 8761	. . . 4 class card
14	12, 13	ccom 5118	. . 3 class ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` om ) o. card )
15		cfn 7955	. . . . 5 class Fin
16	3, 15	cdif 3571	. . . 4 class ( _V \ Fin )
17		cpnf 10071	. . . . 5 class +oo
18	17	csn 4177	. . . 4 class { +oo }
19	16, 18	cxp 5112	. . 3 class ( ( _V \ Fin ) X. { +oo } )
20	14, 19	cun 3572	. 2 class ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )
21	1, 20	wceq 1483	1 wff # = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )

This definition is referenced by:  hashgval  13120  hashinf  13122  hashfxnn0  13124  hashfOLD  13126