Theorem cardon 9935

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

Syntax hints:   ∈ wcel 2107  {cab 2710  ∃wrex 3071   class class class wbr 5147  Oncon0 6361  ‘cfv 6540   ≈ cen 8932  cardccrd 9926

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 5298  ax-nul 5305  ax-pr 5426

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 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 6364  df-on 6365  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-card 9930

This theorem is referenced by:  isnum3  9945  cardidm  9950  ficardom  9952  cardne  9956  carden2b  9958  cardlim  9963  cardsdomelir  9964  cardsdomel  9965  iscard  9966  iscard2  9967  carddom2  9968  carduni  9972  cardom  9977  cardsdom2  9979  domtri2  9980  cardval2  9982  infxpidm2  10008  dfac8b  10022  numdom  10029  indcardi  10032  alephnbtwn  10062  alephnbtwn2  10063  alephsucdom  10070  cardaleph  10080  iscard3  10084  alephinit  10086  alephsson  10091  alephval3  10101  dfac12r  10137  dfac12k  10138  cardadju  10185  djunum  10186  pwsdompw  10195  cff  10239  cardcf  10243  cfon  10246  cfeq0  10247  cfsuc  10248  cff1  10249  cfflb  10250  cflim2  10254  cfss  10256  fin1a2lem9  10399  ttukeylem6  10505  ttukeylem7  10506  unsnen  10544  inar1  10766  tskcard  10772  tskuni  10774  gruina  10809  iscard4  42217  minregex  42218