Theorem cardon 9375

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

Syntax hints:   ∈ wcel 2114  {cab 2801  ∃wrex 3141   class class class wbr 5068  Oncon0 6193  ‘cfv 6357   ≈ cen 8508  cardccrd 9366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-ord 6196  df-on 6197  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365  df-card 9370

This theorem is referenced by:  isnum3  9385  cardidm  9390  ficardom  9392  cardne  9396  carden2b  9398  cardlim  9403  cardsdomelir  9404  cardsdomel  9405  iscard  9406  iscard2  9407  carddom2  9408  carduni  9412  cardom  9417  cardsdom2  9419  domtri2  9420  cardval2  9422  infxpidm2  9445  dfac8b  9459  numdom  9466  indcardi  9469  alephnbtwn  9499  alephnbtwn2  9500  alephsucdom  9507  cardaleph  9517  iscard3  9521  alephinit  9523  alephsson  9528  alephval3  9538  dfac12r  9574  dfac12k  9575  cardadju  9622  djunum  9623  pwsdompw  9628  cff  9672  cardcf  9676  cfon  9679  cfeq0  9680  cfsuc  9681  cff1  9682  cfflb  9683  cflim2  9687  cfss  9689  fin1a2lem9  9832  ttukeylem6  9938  ttukeylem7  9939  unsnen  9977  inar1  10199  tskcard  10205  tskuni  10207  gruina  10242  iscard4  39907