Theorem cardon 9952

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

This proof depends on syntax axioms:   ∈ wcel 2145  {cab 2738  ∃wrex 3086   class class class wbr 5103  Oncon0 6357  ‘cfv 6533   ≈ cen 8952  cardccrd 9943

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6360  df-on 6361  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-card 9947

This theorem is used by:  isnum3  9962  cardidm  9967  ficardom  9969  cardne  9973  carden2b  9975  cardlim  9980  cardsdomelir  9981  cardsdomel  9982  iscard  9983  iscard2  9984  carddom2  9985  carduni  9989  cardom  9994  cardsdom2  9996  domtri2  9997  cardval2  9999  infxpidm2  10023  dfac8b  10037  numdom  10044  indcardi  10047  alephnbtwn  10077  alephnbtwn2  10078  alephsucdom  10085  cardaleph  10095  iscard3  10099  alephinit  10101  alephsson  10106  alephval3  10116  dfac12r  10152  dfac12k  10153  cardadju  10200  djunum  10201  pwsdompw  10208  cff  10252  cardcf  10256  cfonOLD  10260  cfeq0  10261  cfsuc  10262  cff1  10263  cfflb  10264  cflim2  10268  cfss  10270  fin1a2lem9  10413  ttukeylem6  10519  ttukeylem7  10520  unsnen  10564  inar1  10787  tskcard  10793  tskuni  10795  gruina  10830  findcard4  38466  iscard4  44376  minregex  44377