Theorem cardon 9840

Description: The cardinal number of a set is an ordinal number. Proposition 10.6(1) of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) (Revised by Mario Carneiro, 13-Sep-2013.)

Assertion

Ref	Expression
cardon	⊢ (card‘𝐴) ∈ On

Proof of Theorem cardon

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cardf2 9839	. 2 ⊢ card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On
2		0elon 6362	. 2 ⊢ ∅ ∈ On
3	1, 2	f0cli 7032	1 ⊢ (card‘𝐴) ∈ On

Syntax hints:   ∈ wcel 2109  {cab 2707  ∃wrex 3053   class class class wbr 5092  Oncon0 6307  ‘cfv 6482   ≈ cen 8869  cardccrd 9831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6310  df-on 6311  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-card 9835

This theorem is referenced by:  isnum3  9850  cardidm  9855  ficardom  9857  cardne  9861  carden2b  9863  cardlim  9868  cardsdomelir  9869  cardsdomel  9870  iscard  9871  iscard2  9872  carddom2  9873  carduni  9877  cardom  9882  cardsdom2  9884  domtri2  9885  cardval2  9887  infxpidm2  9911  dfac8b  9925  numdom  9932  indcardi  9935  alephnbtwn  9965  alephnbtwn2  9966  alephsucdom  9973  cardaleph  9983  iscard3  9987  alephinit  9989  alephsson  9994  alephval3  10004  dfac12r  10041  dfac12k  10042  cardadju  10089  djunum  10090  pwsdompw  10097  cff  10142  cardcf  10146  cfon  10149  cfeq0  10150  cfsuc  10151  cff1  10152  cfflb  10153  cflim2  10157  cfss  10159  fin1a2lem9  10302  ttukeylem6  10408  ttukeylem7  10409  unsnen  10447  inar1  10669  tskcard  10675  tskuni  10677  gruina  10712  iscard4  43510  minregex  43511