ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ihash Unicode version

Definition df-ihash 10477
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 8311). 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
StepHypRef Expression
1 chash 10476 . 2  class
2 vx . . . . . 6  setvar  x
3 cz 9012 . . . . . 6  class  ZZ
42cv 1315 . . . . . . 7  class  x
5 c1 7589 . . . . . . 7  class  1
6 caddc 7591 . . . . . . 7  class  +
74, 5, 6co 5742 . . . . . 6  class  ( x  +  1 )
82, 3, 7cmpt 3959 . . . . 5  class  ( x  e.  ZZ  |->  ( x  +  1 ) )
9 cc0 7588 . . . . 5  class  0
108, 9cfrec 6255 . . . 4  class frec ( ( x  e.  ZZ  |->  ( x  +  1 ) ) ,  0 )
11 com 4474 . . . . . 6  class  om
12 cpnf 7765 . . . . . 6  class +oo
1311, 12cop 3500 . . . . 5  class  <. om , +oo >.
1413csn 3497 . . . 4  class  { <. om , +oo >. }
1510, 14cun 3039 . . 3  class  (frec ( ( x  e.  ZZ  |->  ( x  +  1
) ) ,  0 )  u.  { <. om , +oo >. } )
16 cvv 2660 . . . 4  class  _V
17 vy . . . . . . . 8  setvar  y
1817cv 1315 . . . . . . 7  class  y
19 cdom 6601 . . . . . . 7  class  ~<_
2018, 4, 19wbr 3899 . . . . . 6  wff  y  ~<_  x
2111csn 3497 . . . . . . 7  class  { om }
2211, 21cun 3039 . . . . . 6  class  ( om  u.  { om }
)
2320, 17, 22crab 2397 . . . . 5  class  { y  e.  ( om  u.  { om } )  |  y  ~<_  x }
2423cuni 3706 . . . 4  class  U. {
y  e.  ( om  u.  { om }
)  |  y  ~<_  x }
252, 16, 24cmpt 3959 . . 3  class  ( x  e.  _V  |->  U. {
y  e.  ( om  u.  { om }
)  |  y  ~<_  x } )
2615, 25ccom 4513 . 2  class  ( (frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )  u.  { <. om , +oo >. } )  o.  ( x  e.  _V  |->  U. {
y  e.  ( om  u.  { om }
)  |  y  ~<_  x } ) )
271, 26wceq 1316 1  wff =  ( (frec ( ( x  e.  ZZ  |->  ( x  +  1 ) ) ,  0 )  u. 
{ <. om , +oo >. } )  o.  (
x  e.  _V  |->  U. { y  e.  ( om  u.  { om } )  |  y  ~<_  x } ) )
Colors of variables: wff set class
This definition is referenced by:  hashinfom  10479  hashennn  10481
  Copyright terms: Public domain W3C validator