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

Theorem onelon 4417
Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
Assertion
Ref Expression
onelon  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )

Proof of Theorem onelon
StepHypRef Expression
1 eloni 4402 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelon 4416 . 2  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  e.  On )
31, 2sylan 459 1  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1685   Ord word 4391   Oncon0 4392
This theorem is referenced by:  oneli  4500  ssorduni  4577  unon  4622  tfindsg2  4652  dfom2  4658  ordom  4665  onfununi  6354  onnseq  6357  tz7.48-2  6450  tz7.49  6453  oalim  6527  omlim  6528  oelim  6529  oaordi  6540  oalimcl  6554  oaass  6555  omordi  6560  omlimcl  6572  odi  6573  omass  6574  omeulem1  6576  omeulem2  6577  omopth2  6578  oewordri  6586  oeordsuc  6588  oelimcl  6594  oeeui  6596  oaabs2  6639  omabs  6641  omxpenlem  6959  hartogs  7255  card2on  7264  cantnfle  7368  cantnflt  7369  cantnfp1lem2  7377  cantnfp1lem3  7378  cantnfp1  7379  oemapvali  7382  cantnflem1b  7384  cantnflem1c  7385  cantnflem1d  7386  cantnflem1  7387  cantnflem2  7388  cantnflem3  7389  cantnflem4  7390  cantnf  7391  cnfcomlem  7398  cnfcom3lem  7402  cnfcom3  7403  r1ordg  7446  r1val3  7506  tskwe  7579  iscard  7604  cardmin2  7627  infxpenlem  7637  infxpenc2lem2  7643  alephordi  7697  alephord2i  7700  alephle  7711  cardaleph  7712  cfub  7871  cfsmolem  7892  zorn2lem5  8123  zorn2lem6  8124  ttukeylem6  8137  ttukeylem7  8138  ondomon  8181  cardmin  8182  alephval2  8190  alephreg  8200  smobeth  8204  winainflem  8311  inar1  8393  inatsk  8396  dfrdg2  23554  tfrALTlem  23678  sltval2  23711  sltres  23719  axdenselem5  23741  axdenselem7  23743  axfelem6  23753  axfelem18  23765  axfelem19  23766  axfelem20  23767  axfelem22  23769  dfrdg4  23896  ontopbas  24275  onpsstopbas  24277  onint1  24296  vtarsu  25286  tartarmap  25288
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4214
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-tr 4116  df-eprel 4305  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396
  Copyright terms: Public domain W3C validator