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

Theorem onenon 8333
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 7549 . 2  |-  ( A  e.  On  ->  A  ~~  A )
2 isnumi 8330 . 2  |-  ( ( A  e.  On  /\  A  ~~  A )  ->  A  e.  dom  card )
31, 2mpdan 668 1  |-  ( A  e.  On  ->  A  e.  dom  card )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   class class class wbr 4437   Oncon0 4868   dom cdm 4989    ~~ cen 7515   cardccrd 8319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-en 7519  df-card 8323
This theorem is referenced by:  oncardval  8339  oncardid  8340  cardnn  8347  iscard  8359  carduni  8365  nnsdomel  8374  harsdom  8379  pm54.43lem  8383  infxpenlem  8394  infxpidm2  8397  onssnum  8424  alephnbtwn  8455  alephnbtwn2  8456  alephordilem1  8457  alephord2  8460  alephsdom  8470  cardaleph  8473  infenaleph  8475  alephinit  8479  iunfictbso  8498  ficardun2  8586  pwsdompw  8587  infunsdom1  8596  ackbij2  8626  cfflb  8642  sdom2en01  8685  fin23lem22  8710  iunctb  8952  alephadd  8955  alephmul  8956  alephexp1  8957  alephsuc3  8958  canthp1lem2  9034  pwfseqlem4a  9042  pwfseqlem4  9043  pwfseqlem5  9044  gchaleph  9052  gchaleph2  9053  hargch  9054  cygctb  16873  ttac  30954  numinfctb  31028  isnumbasgrplem2  31029  isnumbasabl  31031
  Copyright terms: Public domain W3C validator