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

Theorem onelon 4389
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 4374 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelon 4388 . 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 1621   Ord word 4363   Oncon0 4364
This theorem is referenced by:  oneli  4472  ssorduni  4549  unon  4594  tfindsg2  4624  dfom2  4630  ordom  4637  onfununi  6326  onnseq  6329  tz7.48-2  6422  tz7.49  6425  oalim  6499  omlim  6500  oelim  6501  oaordi  6512  oalimcl  6526  oaass  6527  omordi  6532  omlimcl  6544  odi  6545  omass  6546  omeulem1  6548  omeulem2  6549  omopth2  6550  oewordri  6558  oeordsuc  6560  oelimcl  6566  oeeui  6568  oaabs2  6611  omabs  6613  omxpenlem  6931  hartogs  7227  card2on  7236  cantnfle  7340  cantnflt  7341  cantnfp1lem2  7349  cantnfp1lem3  7350  cantnfp1  7351  oemapvali  7354  cantnflem1b  7356  cantnflem1c  7357  cantnflem1d  7358  cantnflem1  7359  cantnflem2  7360  cantnflem3  7361  cantnflem4  7362  cantnf  7363  cnfcomlem  7370  cnfcom3lem  7374  cnfcom3  7375  r1ordg  7418  r1val3  7478  tskwe  7551  iscard  7576  cardmin2  7599  infxpenlem  7609  infxpenc2lem2  7615  alephordi  7669  alephord2i  7672  alephle  7683  cardaleph  7684  cfub  7843  cfsmolem  7864  zorn2lem5  8095  zorn2lem6  8096  ttukeylem6  8109  ttukeylem7  8110  ondomon  8153  cardmin  8154  alephval2  8162  alephreg  8172  smobeth  8176  winainflem  8283  inar1  8365  inatsk  8368  dfrdg2  23521  tfrALTlem  23645  sltval2  23678  sltres  23686  axdenselem5  23708  axdenselem7  23710  axfelem6  23720  axfelem18  23732  axfelem19  23733  axfelem20  23734  axfelem22  23736  dfrdg4  23863  ontopbas  24242  onpsstopbas  24244  onint1  24263  vtarsu  25253  tartarmap  25255
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-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-tr 4088  df-eprel 4277  df-po 4286  df-so 4287  df-fr 4324  df-we 4326  df-ord 4367  df-on 4368
  Copyright terms: Public domain W3C validator