Theorem cardon 9941

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

Syntax hints:   ∈ wcel 2104  {cab 2707  ∃wrex 3068   class class class wbr 5147  Oncon0 6363  ‘cfv 6542   ≈ cen 8938  cardccrd 9932

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-card 9936

This theorem is referenced by:  isnum3  9951  cardidm  9956  ficardom  9958  cardne  9962  carden2b  9964  cardlim  9969  cardsdomelir  9970  cardsdomel  9971  iscard  9972  iscard2  9973  carddom2  9974  carduni  9978  cardom  9983  cardsdom2  9985  domtri2  9986  cardval2  9988  infxpidm2  10014  dfac8b  10028  numdom  10035  indcardi  10038  alephnbtwn  10068  alephnbtwn2  10069  alephsucdom  10076  cardaleph  10086  iscard3  10090  alephinit  10092  alephsson  10097  alephval3  10107  dfac12r  10143  dfac12k  10144  cardadju  10191  djunum  10192  pwsdompw  10201  cff  10245  cardcf  10249  cfon  10252  cfeq0  10253  cfsuc  10254  cff1  10255  cfflb  10256  cflim2  10260  cfss  10262  fin1a2lem9  10405  ttukeylem6  10511  ttukeylem7  10512  unsnen  10550  inar1  10772  tskcard  10778  tskuni  10780  gruina  10815  iscard4  42586  minregex  42587