MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-aleph Structured version   Visualization version   Unicode version

Definition df-aleph 8399
Description: Define the aleph function. Our definition expresses Definition 12 of [Suppes] p. 229 in a closed form, from which we derive the recursive definition as theorems aleph0 8522, alephsuc 8524, and alephlim 8523. The aleph function provides a one-to-one, onto mapping from the ordinal numbers to the infinite cardinal numbers. Roughly, any aleph is the smallest infinite cardinal number whose size is strictly greater than any aleph before it. (Contributed by NM, 21-Oct-2003.)
Assertion
Ref Expression
df-aleph  |-  aleph  =  rec (har ,  om )

Detailed syntax breakdown of Definition df-aleph
StepHypRef Expression
1 cale 8395 . 2  class  aleph
2 char 8096 . . 3  class har
3 com 6718 . . 3  class  om
42, 3crdg 7152 . 2  class  rec (har ,  om )
51, 4wceq 1454 1  wff  aleph  =  rec (har ,  om )
Colors of variables: wff setvar class
This definition is referenced by:  alephfnon  8521  aleph0  8522  alephlim  8523  alephsuc  8524
  Copyright terms: Public domain W3C validator