# Metamath Proof Explorer

## Theorem aleph0

Description: The first infinite cardinal number, discovered by Georg Cantor in 1873, has the same size as the set of natural numbers _om (and under our particular definition is also equal to it). In the literature, the argument of the aleph function is often written as a subscript, and the first aleph is written aleph_0. Exercise 3 of TakeutiZaring p. 91. Also Definition 12(i) of Suppes p. 228. From Moshé Machover,Set Theory, Logic, and Their Limitations, p. 95: "Aleph...the first letter in the Hebrew alphabet...is also the first letter of the Hebrew word...(_einsoph_, meaning infinity), which is a cabbalistic appellation of the deity. The notation is due to Cantor, who was deeply interested in mysticism." (Contributed by NM, 21-Oct-2003) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Assertion aleph0 ${⊢}\aleph \left(\varnothing \right)=\mathrm{\omega }$

### Proof

Step Hyp Ref Expression
1 df-aleph ${⊢}\aleph =\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)$
2 1 fveq1i ${⊢}\aleph \left(\varnothing \right)=\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(\varnothing \right)$
3 omex ${⊢}\mathrm{\omega }\in \mathrm{V}$
4 3 rdg0 ${⊢}\mathrm{rec}\left(\mathrm{har},\mathrm{\omega }\right)\left(\varnothing \right)=\mathrm{\omega }$
5 2 4 eqtri ${⊢}\aleph \left(\varnothing \right)=\mathrm{\omega }$