Theorem cardon 9897

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

Syntax hints:   ∈ wcel 2109  {cab 2707  ∃wrex 3053   class class class wbr 5107  Oncon0 6332  ‘cfv 6511   ≈ cen 8915  cardccrd 9888

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-card 9892

This theorem is referenced by:  isnum3  9907  cardidm  9912  ficardom  9914  cardne  9918  carden2b  9920  cardlim  9925  cardsdomelir  9926  cardsdomel  9927  iscard  9928  iscard2  9929  carddom2  9930  carduni  9934  cardom  9939  cardsdom2  9941  domtri2  9942  cardval2  9944  infxpidm2  9970  dfac8b  9984  numdom  9991  indcardi  9994  alephnbtwn  10024  alephnbtwn2  10025  alephsucdom  10032  cardaleph  10042  iscard3  10046  alephinit  10048  alephsson  10053  alephval3  10063  dfac12r  10100  dfac12k  10101  cardadju  10148  djunum  10149  pwsdompw  10156  cff  10201  cardcf  10205  cfon  10208  cfeq0  10209  cfsuc  10210  cff1  10211  cfflb  10212  cflim2  10216  cfss  10218  fin1a2lem9  10361  ttukeylem6  10467  ttukeylem7  10468  unsnen  10506  inar1  10728  tskcard  10734  tskuni  10736  gruina  10771  iscard4  43522  minregex  43523