Theorem aleph0 4786

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₀. Exercise 3 of [TakeutiZaring] p. 91. Also Definition 12(i) of [Suppes] p. 228. From Kuratowski and Mostowski, Set Theory, 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."

Assertion

Ref	Expression
aleph0	|- (aleph` (/)) = om

Proof of Theorem aleph0

Step	Hyp	Ref	Expression
1		df-aleph 4741	. . 3 |- aleph = rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)
2	1	fveq1i 3664	. 2 |- (aleph` (/)) = (rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)` (/))
3		omex 4551	. . 3 |- om e. V
4	3	rdg0 3880	. 2 |- (rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)` (/)) = om
5	2, 4	eqtr 1471	1 |- (aleph` (/)) = om

Syntax hints:   = wceq 1099  {crab 1624  (/)c0 2251  |^|cint 2501   class class class wbr 2587  {copab 2634  Oncon0 2911  omcom 3094  ` cfv 3145  reccrdg 3870   ~< csdm 4304  alephcale 4738

This theorem is referenced by:  alephon 4788  alephcard 4790  alephgeom 4805  cardaleph 4808  aleph1re 7445

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-rab 1628  df-v 1787  df-sbc 1913  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-fv 3161  df-rdg 3871  df-aleph 4741

Copyright terms: Public domain