Theorem ontr1 6362

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Ord word 6314  Oncon0 6315

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-v 3440  df-ss 3916  df-uni 4862  df-tr 5204  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319

This theorem is referenced by:  epweon  7718  smoiun  8291  dif20el  8430  oeordi  8513  omabs  8577  omsmolem  8583  naddel12  8626  naddsuc2  8627  cofsmo  10177  cfsmolem  10178  inar1  10684  grur1a  10728  nosupno  27669  nosupbnd2lem1  27681  noinfno  27684  noinfbnd2lem1  27696  lrrecpo  27911  addsproplem2  27940  r1elcl  35203  onexoegt  43428  oneltr  43440  oaun3lem1  43558  nadd2rabtr  43568  naddwordnexlem0  43580  oawordex3  43584  naddwordnexlem4  43585