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

Theorem ordelon 6388
Description: An element of an ordinal class is an ordinal number. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.)
Assertion
Ref Expression
ordelon ((Ord 𝐴𝐵𝐴) → 𝐵 ∈ On)

Proof of Theorem ordelon
StepHypRef Expression
1 ordelord 6386 . 2 ((Ord 𝐴𝐵𝐴) → Ord 𝐵)
2 elong 6372 . . 3 (𝐵𝐴 → (𝐵 ∈ On ↔ Ord 𝐵))
32adantl 482 . 2 ((Ord 𝐴𝐵𝐴) → (𝐵 ∈ On ↔ Ord 𝐵))
41, 3mpbird 256 1 ((Ord 𝐴𝐵𝐴) → 𝐵 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wcel 2106  Ord word 6363  Oncon0 6364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368
This theorem is referenced by:  onelon  6389  ordunidif  6413  ordpwsuc  7805  ordsucun  7815  ordunel  7817  ordunisuc2  7835  oesuclem  8527  odi  8581  oelim2  8597  oeoalem  8598  oeoelem  8600  limenpsi  9154  ordtypelem9  9523  oismo  9537  cantnflt  9669  cantnfp1lem3  9677  cantnflem1b  9683  cantnflem1  9686  rankr1bg  9800  rankr1clem  9817  rankr1c  9818  rankonidlem  9825  infxpenlem  10010  coflim  10258  fin23lem26  10322  fpwwe2lem7  10634  onsuct0  35629  ordnexbtwnsuc  42319  orddif0suc  42320  omord2lim  42352  nadd2rabtr  42436  nadd2rabex  42438  nadd1rabtr  42440  nadd1rabex  42442  iunord  47809
  Copyright terms: Public domain W3C validator