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

Theorem ontr1 6432
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 6396 . 2 (𝐶 ∈ On → Ord 𝐶)
2 ordtr1 6429 . 2 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (𝐶 ∈ On → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2106  Ord word 6385  Oncon0 6386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-v 3480  df-ss 3980  df-uni 4913  df-tr 5266  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390
This theorem is referenced by:  epweon  7794  smoiun  8400  dif20el  8542  oeordi  8624  omabs  8688  omsmolem  8694  naddel12  8737  naddsuc2  8738  cofsmo  10307  cfsmolem  10308  inar1  10813  grur1a  10857  nosupno  27763  nosupbnd2lem1  27775  noinfno  27778  noinfbnd2lem1  27790  lrrecpo  27989  addsproplem2  28018  onexoegt  43233  oneltr  43245  oaun3lem1  43364  nadd2rabtr  43374  naddwordnexlem0  43386  oawordex3  43390  naddwordnexlem4  43391
  Copyright terms: Public domain W3C validator