Definition df-ihash 10758

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 8541). 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 10757	. 2 class ♯
2		vx	. . . . . 6 setvar x
3		cz 9255	. . . . . 6 class ZZ
4	2	cv 1352	. . . . . . 7 class x
5		c1 7814	. . . . . . 7 class 1
6		caddc 7816	. . . . . . 7 class +
7	4, 5, 6	co 5877	. . . . . 6 class ( x + 1 )
8	2, 3, 7	cmpt 4066	. . . . 5 class ( x e. ZZ |-> ( x + 1 ) )
9		cc0 7813	. . . . 5 class 0
10	8, 9	cfrec 6393	. . . 4 class frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )
11		com 4591	. . . . . 6 class om
12		cpnf 7991	. . . . . 6 class +oo
13	11, 12	cop 3597	. . . . 5 class <. om , +oo >.
14	13	csn 3594	. . . 4 class { <. om , +oo >. }
15	10, 14	cun 3129	. . 3 class (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } )
16		cvv 2739	. . . 4 class _V
17		vy	. . . . . . . 8 setvar y
18	17	cv 1352	. . . . . . 7 class y
19		cdom 6741	. . . . . . 7 class ~<_
20	18, 4, 19	wbr 4005	. . . . . 6 wff y ~<_ x
21	11	csn 3594	. . . . . . 7 class { om }
22	11, 21	cun 3129	. . . . . 6 class ( om u. { om } )
23	20, 17, 22	crab 2459	. . . . 5 class { y e. ( om u. { om } ) | y ~<_ x }
24	23	cuni 3811	. . . 4 class U. { y e. ( om u. { om } ) | y ~<_ x }
25	2, 16, 24	cmpt 4066	. . 3 class ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } )
26	15, 25	ccom 4632	. 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 1353	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  10760  hashennn  10762