Theorem ontr1 6370

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Ord word 6322  Oncon0 6323

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-ss 3906  df-uni 4851  df-tr 5193  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327

This theorem is referenced by:  epweon  7729  smoiun  8301  dif20el  8440  oeordi  8523  omabs  8587  omsmolem  8593  naddel12  8636  naddsuc2  8637  cofsmo  10191  cfsmolem  10192  inar1  10698  grur1a  10742  nosupno  27667  nosupbnd2lem1  27679  noinfno  27682  noinfbnd2lem1  27694  lrrecpo  27933  addsproplem2  27962  r1elcl  35241  onexoegt  43672  oneltr  43684  oaun3lem1  43802  nadd2rabtr  43812  naddwordnexlem0  43824  oawordex3  43828  naddwordnexlem4  43829