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

Theorem ontr1 6429
Description: Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by NM, 11-Aug-1994.)
Assertion
Ref Expression
ontr1 (𝐶 ∈ On → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))

Proof of Theorem ontr1
StepHypRef Expression
1 eloni 6393 . 2 (𝐶 ∈ On → Ord 𝐶)
2 ordtr1 6426 . 2 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (𝐶 ∈ On → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2107  Ord word 6382  Oncon0 6383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-v 3481  df-ss 3967  df-uni 4907  df-tr 5259  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-ord 6386  df-on 6387
This theorem is referenced by:  epweon  7796  smoiun  8402  dif20el  8544  oeordi  8626  omabs  8690  omsmolem  8696  naddel12  8739  naddsuc2  8740  cofsmo  10310  cfsmolem  10311  inar1  10816  grur1a  10860  nosupno  27749  nosupbnd2lem1  27761  noinfno  27764  noinfbnd2lem1  27776  lrrecpo  27975  addsproplem2  28004  onexoegt  43261  oneltr  43273  oaun3lem1  43392  nadd2rabtr  43402  naddwordnexlem0  43414  oawordex3  43418  naddwordnexlem4  43419
  Copyright terms: Public domain W3C validator