Theorem cardon 9873

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 9872	. 2 ⊢ card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On
2		0elon 6375	. 2 ⊢ ∅ ∈ On
3	1, 2	f0cli 7052	1 ⊢ (card‘𝐴) ∈ On

Syntax hints:   ∈ wcel 2109  {cab 2707  ∃wrex 3053   class class class wbr 5102  Oncon0 6320  ‘cfv 6499   ≈ cen 8892  cardccrd 9864

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6323  df-on 6324  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-card 9868

This theorem is referenced by:  isnum3  9883  cardidm  9888  ficardom  9890  cardne  9894  carden2b  9896  cardlim  9901  cardsdomelir  9902  cardsdomel  9903  iscard  9904  iscard2  9905  carddom2  9906  carduni  9910  cardom  9915  cardsdom2  9917  domtri2  9918  cardval2  9920  infxpidm2  9946  dfac8b  9960  numdom  9967  indcardi  9970  alephnbtwn  10000  alephnbtwn2  10001  alephsucdom  10008  cardaleph  10018  iscard3  10022  alephinit  10024  alephsson  10029  alephval3  10039  dfac12r  10076  dfac12k  10077  cardadju  10124  djunum  10125  pwsdompw  10132  cff  10177  cardcf  10181  cfon  10184  cfeq0  10185  cfsuc  10186  cff1  10187  cfflb  10188  cflim2  10192  cfss  10194  fin1a2lem9  10337  ttukeylem6  10443  ttukeylem7  10444  unsnen  10482  inar1  10704  tskcard  10710  tskuni  10712  gruina  10747  iscard4  43515  minregex  43516