Definition df-ihash 10710

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.

Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8501). We adopt the former notation from Corollary 8.2.4 of [AczelRathjen], p. 80 (although that work only defines it for finite sets).

This definition (in terms of U. and ~<_) is not taken directly from the literature, but for finite sets should be equivalent to the conventional definition that the size of a finite set is the unique natural number which is equinumerous to the given set. (Contributed by Jim Kingdon, 19-Feb-2022.)

Assertion

Ref	Expression
df-ihash	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-ihash

Step	Hyp	Ref	Expression
1		chash 10709	. 2 class ♯
2		vx	. . . . . 6 setvar x
3		cz 9212	. . . . . 6 class ZZ
4	2	cv 1347	. . . . . . 7 class x
5		c1 7775	. . . . . . 7 class 1
6		caddc 7777	. . . . . . 7 class +
7	4, 5, 6	co 5853	. . . . . 6 class ( x + 1 )
8	2, 3, 7	cmpt 4050	. . . . 5 class ( x e. ZZ |-> ( x + 1 ) )
9		cc0 7774	. . . . 5 class 0
10	8, 9	cfrec 6369	. . . 4 class frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )
11		com 4574	. . . . . 6 class om
12		cpnf 7951	. . . . . 6 class +oo
13	11, 12	cop 3586	. . . . 5 class <. om , +oo >.
14	13	csn 3583	. . . 4 class { <. om , +oo >. }
15	10, 14	cun 3119	. . 3 class (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } )
16		cvv 2730	. . . 4 class _V
17		vy	. . . . . . . 8 setvar y
18	17	cv 1347	. . . . . . 7 class y
19		cdom 6717	. . . . . . 7 class ~<_
20	18, 4, 19	wbr 3989	. . . . . 6 wff y ~<_ x
21	11	csn 3583	. . . . . . 7 class { om }
22	11, 21	cun 3119	. . . . . 6 class ( om u. { om } )
23	20, 17, 22	crab 2452	. . . . 5 class { y e. ( om u. { om } ) | y ~<_ x }
24	23	cuni 3796	. . . 4 class U. { y e. ( om u. { om } ) | y ~<_ x }
25	2, 16, 24	cmpt 4050	. . 3 class ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } )
26	15, 25	ccom 4615	. 2 class ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
27	1, 26	wceq 1348	1 wff ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )

This definition is referenced by:  hashinfom  10712  hashennn  10714