Theorem cardon 10035

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

This proof depends on syntax axioms:   ∈ wcel 2146  {cab 2741  ∃wrex 3089   class class class wbr 5105  Oncon0 6368  ‘cfv 6546   ≈ cen 8981  cardccrd 10026

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-int 4910  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-ord 6371  df-on 6372  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-card 10030

This theorem is used by:  isnum3  10045  cardidm  10050  ficardom  10052  cardne  10056  carden2b  10058  cardlim  10063  cardsdomelir  10064  cardsdomel  10065  iscard  10066  iscard2  10067  carddom2  10068  carduni  10072  cardom  10077  cardsdom2  10079  domtri2  10080  cardval2  10082  infxpidm2  10106  dfac8b  10120  numdom  10127  indcardi  10130  alephnbtwn  10160  alephnbtwn2  10161  alephsucdom  10168  cardaleph  10178  iscard3  10182  alephinit  10184  alephsson  10189  alephval3  10199  dfac12r  10235  dfac12k  10236  cardadju  10283  djunum  10284  pwsdompw  10291  cff  10335  cardcf  10339  cfonOLD  10343  cfeq0  10344  cfsuc  10345  cff1  10346  cfflb  10347  cflim2  10351  cfss  10353  fin1a2lem9  10496  ttukeylem6  10602  ttukeylem7  10603  unsnen  10647  inar1  10870  tskcard  10876  tskuni  10878  gruina  10913  unidifsnel  33185  unidifsnne  33186  findcard4  38772  iscard4  44674  minregex  44675