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

Theorem onenon 8261
Description: Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
onenon  |-  ( A  e.  On  ->  A  e.  dom  card )

Proof of Theorem onenon
StepHypRef Expression
1 enrefg 7484 . 2  |-  ( A  e.  On  ->  A  ~~  A )
2 isnumi 8258 . 2  |-  ( ( A  e.  On  /\  A  ~~  A )  ->  A  e.  dom  card )
31, 2mpdan 666 1  |-  ( A  e.  On  ->  A  e.  dom  card )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1836   class class class wbr 4380   Oncon0 4805   dom cdm 4926    ~~ cen 7450   cardccrd 8247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-int 4213  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-en 7454  df-card 8251
This theorem is referenced by:  oncardval  8267  oncardid  8268  cardnn  8275  iscard  8287  carduni  8293  nnsdomel  8302  harsdom  8307  pm54.43lem  8311  infxpenlem  8322  infxpidm2  8325  onssnum  8352  alephnbtwn  8383  alephnbtwn2  8384  alephordilem1  8385  alephord2  8388  alephsdom  8398  cardaleph  8401  infenaleph  8403  alephinit  8407  iunfictbso  8426  ficardun2  8514  pwsdompw  8515  infunsdom1  8524  ackbij2  8554  cfflb  8570  sdom2en01  8613  fin23lem22  8638  iunctb  8880  alephadd  8883  alephmul  8884  alephexp1  8885  alephsuc3  8886  canthp1lem2  8960  pwfseqlem4a  8968  pwfseqlem4  8969  pwfseqlem5  8970  gchaleph  8978  gchaleph2  8979  hargch  8980  cygctb  17030  ttac  31180  numinfctb  31256  isnumbasgrplem2  31257  isnumbasabl  31259
  Copyright terms: Public domain W3C validator