Theorem ontr1 6353

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 6316	. 2 ⊢ (𝐶 ∈ On → Ord 𝐶)
2		ordtr1 6350	. 2 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Ord word 6305  Oncon0 6306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-ss 3914  df-uni 4857  df-tr 5197  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6309  df-on 6310

This theorem is referenced by:  epweon  7708  smoiun  8281  dif20el  8420  oeordi  8502  omabs  8566  omsmolem  8572  naddel12  8615  naddsuc2  8616  cofsmo  10160  cfsmolem  10161  inar1  10666  grur1a  10710  nosupno  27642  nosupbnd2lem1  27654  noinfno  27657  noinfbnd2lem1  27669  lrrecpo  27884  addsproplem2  27913  r1elcl  35109  onexoegt  43347  oneltr  43359  oaun3lem1  43477  nadd2rabtr  43487  naddwordnexlem0  43499  oawordex3  43503  naddwordnexlem4  43504