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

Theorem onelon 4641
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 4626 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelon 4640 . 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 4    /\ wa 360    e. wcel 1728   Ord word 4615   Oncon0 4616
This theorem is referenced by:  oneli  4724  ssorduni  4801  unon  4846  tfindsg2  4876  dfom2  4882  ordom  4889  onfununi  6639  onnseq  6642  tz7.48-2  6735  tz7.49  6738  oalim  6812  omlim  6813  oelim  6814  oaordi  6825  oalimcl  6839  oaass  6840  omordi  6845  omlimcl  6857  odi  6858  omass  6859  omeulem1  6861  omeulem2  6862  omopth2  6863  oewordri  6871  oeordsuc  6873  oelimcl  6879  oeeui  6881  oaabs2  6924  omabs  6926  omxpenlem  7245  hartogs  7549  card2on  7558  cantnfle  7662  cantnflt  7663  cantnfp1lem2  7671  cantnfp1lem3  7672  cantnfp1  7673  oemapvali  7676  cantnflem1b  7678  cantnflem1c  7679  cantnflem1d  7680  cantnflem1  7681  cantnflem2  7682  cantnflem3  7683  cantnflem4  7684  cantnf  7685  cnfcomlem  7692  cnfcom3lem  7696  cnfcom3  7697  r1ordg  7740  r1val3  7800  tskwe  7875  iscard  7900  cardmin2  7923  infxpenlem  7933  infxpenc2lem2  7939  alephordi  7993  alephord2i  7996  alephle  8007  cardaleph  8008  cfub  8167  cfsmolem  8188  zorn2lem5  8418  zorn2lem6  8419  ttukeylem6  8432  ttukeylem7  8433  ondomon  8476  cardmin  8477  alephval2  8485  alephreg  8495  smobeth  8499  winainflem  8606  inar1  8688  inatsk  8691  dfrdg2  25458  sltval2  25646  sltres  25654  nodenselem5  25675  nodenselem7  25677  nobndlem6  25687  nobndup  25690  dfrdg4  25830  ontopbas  26213  onpsstopbas  26215  onint1  26234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pr 4438
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-br 4244  df-opab 4298  df-tr 4334  df-eprel 4529  df-po 4538  df-so 4539  df-fr 4576  df-we 4578  df-ord 4619  df-on 4620
  Copyright terms: Public domain W3C validator