Theorem cardon 9105

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

Syntax hints:   ∈ wcel 2107  {cab 2763  ∃wrex 3091   class class class wbr 4888  Oncon0 5978  ‘cfv 6137   ≈ cen 8240  cardccrd 9096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-ord 5981  df-on 5982  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-fv 6145  df-card 9100

This theorem is referenced by:  isnum3  9115  cardidm  9120  ficardom  9122  cardne  9126  carden2b  9128  cardlim  9133  cardsdomelir  9134  cardsdomel  9135  iscard  9136  iscard2  9137  carddom2  9138  carduni  9142  cardom  9147  cardsdom2  9149  domtri2  9150  cardval2  9152  infxpidm2  9175  dfac8b  9189  numdom  9196  indcardi  9199  alephnbtwn  9229  alephnbtwn2  9230  alephsucdom  9237  cardaleph  9247  iscard3  9251  alephinit  9253  alephsson  9258  alephval3  9268  dfac12r  9305  dfac12k  9306  cardacda  9357  cdanum  9358  pwsdompw  9363  cff  9407  cardcf  9411  cfon  9414  cfeq0  9415  cfsuc  9416  cff1  9417  cfflb  9418  cflim2  9422  cfss  9424  fin1a2lem9  9567  ttukeylem6  9673  ttukeylem7  9674  unsnen  9712  inar1  9934  tskcard  9940  tskuni  9942  gruina  9977