Theorem ontr1 6393

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

Step	Hyp	Ref	Expression
1		eloni 6356	. 2 ⊢ (𝐶 ∈ On → Ord 𝐶)
2		ordtr1 6390	. 2 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  Ord word 6345  Oncon0 6346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-v 3456  df-ss 3921  df-uni 4866  df-tr 5208  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6349  df-on 6350

This theorem is referenced by:  epweon  7758  smoiun  8332  dif20el  8474  oeordi  8557  omabs  8621  omsmolem  8627  naddel12  8671  naddsuc2  8672  cofsmo  10226  cfsmolem  10227  inar1  10733  grur1a  10777  nosupno  27767  nosupbnd2lem1  27779  noinfno  27782  noinfbnd2lem1  27794  lrrecpo  28034  addsproplem2  28063  r1elcl  35394  onexoegt  43821  oneltr  43833  oaun3lem1  43951  nadd2rabtr  43961  naddwordnexlem0  43973  oawordex3  43977  naddwordnexlem4  43978