MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  onelon Structured version   Visualization version   GIF version

Theorem onelon 6347
Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.)
Assertion
Ref Expression
onelon ((𝐴 ∈ On ∧ 𝐵𝐴) → 𝐵 ∈ On)

Proof of Theorem onelon
StepHypRef Expression
1 eloni 6332 . 2 (𝐴 ∈ On → Ord 𝐴)
2 ordelon 6346 . 2 ((Ord 𝐴𝐵𝐴) → 𝐵 ∈ On)
31, 2sylan 581 1 ((𝐴 ∈ On ∧ 𝐵𝐴) → 𝐵 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  Ord word 6321  Oncon0 6322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-tr 5228  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-ord 6325  df-on 6326
This theorem is referenced by:  oneli  6436  ssorduni  7718  unon  7771  tfindsg2  7803  dfom2  7809  trom  7816  onfununi  8292  onnseq  8295  dfrecs3  8323  dfrecs3OLD  8324  tz7.48-2  8393  tz7.49  8396  oalim  8483  omlim  8484  oelim  8485  oaordi  8498  oalimcl  8512  oaass  8513  omordi  8518  omlimcl  8530  odi  8531  omass  8532  omeulem1  8534  omeulem2  8535  omopth2  8536  oewordri  8544  oeordsuc  8546  oelimcl  8552  oeeui  8554  oaabs2  8600  omabs  8602  naddssim  8636  naddel12  8651  omxpenlem  9024  hartogs  9487  card2on  9497  cantnfle  9614  cantnflt  9615  cantnfp1lem3  9623  cantnfp1  9624  oemapvali  9627  cantnflem1b  9629  cantnflem1c  9630  cantnflem1d  9631  cantnflem1  9632  cantnflem2  9633  cantnflem3  9634  cantnflem4  9635  cantnf  9636  cnfcomlem  9642  cnfcom3lem  9646  cnfcom3  9647  r1ordg  9721  r1val3  9781  tskwe  9893  iscard  9918  cardmin2  9942  infxpenlem  9956  infxpenc2lem2  9963  alephordi  10017  alephord2i  10020  alephle  10031  cardaleph  10032  cfub  10192  cfsmolem  10213  zorn2lem5  10443  zorn2lem6  10444  ttukeylem6  10457  ttukeylem7  10458  ondomon  10506  cardmin  10507  alephval2  10515  alephreg  10525  smobeth  10529  winainflem  10636  inar1  10718  inatsk  10721  sltval2  27020  sltres  27026  nosepeq  27049  nosupno  27067  nosupres  27071  nosupbnd1lem1  27072  nosupbnd2lem1  27079  nosupbnd2  27080  noinfno  27082  noinfres  27086  noinfbnd1lem1  27087  noinfbnd2lem1  27094  noinfbnd2  27095  oldlim  27238  oldbday  27252  dfrdg2  34409  dfrdg4  34565  ontopbas  34929  onpsstopbas  34931  onint1  34950  onelord  41614  cantnfresb  41688  oawordex2  41690  oacl2g  41694  omabs2  41696  omcl2  41697  ofoafg  41699  ofoaass  41705  oaun3lem1  41719  oaun3lem2  41720  oadif1lem  41724  oadif1  41725  nadd2rabtr  41729  nadd1suc  41737  naddsuc2  41738  naddgeoa  41740  naddwordnexlem0  41742  naddwordnexlem1  41743  naddwordnexlem3  41745  oawordex3  41746  naddwordnexlem4  41747  omssrncard  41886
  Copyright terms: Public domain W3C validator