Theorem cardon 10025

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

This proof depends on syntax axioms:   ∈ wcel 2145  {cab 2739  ∃wrex 3087   class class class wbr 5103  Oncon0 6362  ‘cfv 6538   ≈ cen 8970  cardccrd 10016

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6365  df-on 6366  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-card 10020

This theorem is used by:  isnum3  10035  cardidm  10040  ficardom  10042  cardne  10046  carden2b  10048  cardlim  10053  cardsdomelir  10054  cardsdomel  10055  iscard  10056  iscard2  10057  carddom2  10058  carduni  10062  cardom  10067  cardsdom2  10069  domtri2  10070  cardval2  10072  infxpidm2  10096  dfac8b  10110  numdom  10117  indcardi  10120  alephnbtwn  10150  alephnbtwn2  10151  alephsucdom  10158  cardaleph  10168  iscard3  10172  alephinit  10174  alephsson  10179  alephval3  10189  dfac12r  10225  dfac12k  10226  cardadju  10273  djunum  10274  pwsdompw  10281  cff  10325  cardcf  10329  cfonOLD  10333  cfeq0  10334  cfsuc  10335  cff1  10336  cfflb  10337  cflim2  10341  cfss  10343  fin1a2lem9  10486  ttukeylem6  10592  ttukeylem7  10593  unsnen  10637  inar1  10860  tskcard  10866  tskuni  10868  gruina  10903  findcard4  38632  iscard4  44533  minregex  44534