Theorem aleph0 5670

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."

Assertion

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

Proof of Theorem aleph0

Step	Hyp	Ref	Expression
1		df-aleph 5659	. . 3 |- aleph = rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)
2	1	fveq1i 4493	. 2 |- (aleph` (/)) = (rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)` (/))
3		omex 5542	. . 3 |- om e. _V
4	3	rdg0 4960	. 2 |- (rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)` (/)) = om
5	2, 4	eqtri 1745	1 |- (aleph` (/)) = om

Syntax hints:   = wceq 1136  {crab 1942  (/)c0 2701  |^|cint 3036   class class class wbr 3158  {copab 3213  Oncon0 3472  omcom 3760  ` cfv 3809  reccrdg 4950   ~< csdm 5236  alephcale 5656

This theorem is referenced by:  alephon 5672  elomsubsd 5681  omsublim 5683  infenomsub 5685  alephcard 5811  alephgeom 5826  cardaleph 5829  aleph1re 8615  elomsubsdOLD 15076  omsublimOLD 15078  infenomsubOLD 15080

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601  ax-inf2 5540

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-rab 1946  df-v 2127  df-sbc 2287  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-iun 3079  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-fv 3825  df-rdg 4951  df-aleph 5659

Copyright terms: Public domain