Theorem cardon 9936

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

Syntax hints:   ∈ wcel 2107  {cab 2710  ∃wrex 3071   class class class wbr 5148  Oncon0 6362  ‘cfv 6541   ≈ cen 8933  cardccrd 9927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6365  df-on 6366  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-card 9931

This theorem is referenced by:  isnum3  9946  cardidm  9951  ficardom  9953  cardne  9957  carden2b  9959  cardlim  9964  cardsdomelir  9965  cardsdomel  9966  iscard  9967  iscard2  9968  carddom2  9969  carduni  9973  cardom  9978  cardsdom2  9980  domtri2  9981  cardval2  9983  infxpidm2  10009  dfac8b  10023  numdom  10030  indcardi  10033  alephnbtwn  10063  alephnbtwn2  10064  alephsucdom  10071  cardaleph  10081  iscard3  10085  alephinit  10087  alephsson  10092  alephval3  10102  dfac12r  10138  dfac12k  10139  cardadju  10186  djunum  10187  pwsdompw  10196  cff  10240  cardcf  10244  cfon  10247  cfeq0  10248  cfsuc  10249  cff1  10250  cfflb  10251  cflim2  10255  cfss  10257  fin1a2lem9  10400  ttukeylem6  10506  ttukeylem7  10507  unsnen  10545  inar1  10767  tskcard  10773  tskuni  10775  gruina  10810  iscard4  42270  minregex  42271