MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cardon Unicode version

Theorem cardon 7531
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 `  A )  e.  On

Proof of Theorem cardon
StepHypRef Expression
1 cardf2 7530 . 2  |-  card : {
x  |  E. y  e.  On  y  ~~  x }
--> On
2 0elon 4403 . 2  |-  (/)  e.  On
31, 2f0cli 5591 1  |-  ( card `  A )  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   {cab 2242   E.wrex 2517   class class class wbr 3983   Oncon0 4350   ` cfv 4659    ~~ cen 6814   cardccrd 7522
This theorem is referenced by:  isnum3  7541  cardidm  7546  ficardom  7548  cardne  7552  carden2b  7554  cardlim  7559  cardsdomelir  7560  cardsdomel  7561  iscard  7562  iscard2  7563  carddom2  7564  carduni  7568  cardom  7573  cardsdom2  7575  domtri2  7576  cardval2  7578  infxpidm2  7598  dfac8b  7612  numdom  7619  indcardi  7622  alephnbtwn  7652  alephnbtwn2  7653  alephsucdom  7660  cardaleph  7670  iscard3  7674  alephinit  7676  alephsson  7681  alephval3  7691  dfac12r  7726  dfac12k  7727  cardacda  7778  cdanum  7779  pwsdompw  7784  cff  7828  cardcf  7832  cfon  7835  cfeq0  7836  cfsuc  7837  cff1  7838  cfflb  7839  cflim2  7843  cfss  7845  fin1a2lem9  7988  ttukeylem6  8095  ttukeylem7  8096  unsnen  8129  inar1  8351  tskcard  8357  tskuni  8359  gruina  8394  mreexexd  13498
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-sbc 2953  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-int 3823  df-br 3984  df-opab 4038  df-mpt 4039  df-tr 4074  df-eprel 4263  df-id 4267  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-fv 4675  df-card 7526
  Copyright terms: Public domain W3C validator