Theorem ontr1 6429

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  Ord word 6382  Oncon0 6383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-v 3481  df-ss 3967  df-uni 4907  df-tr 5259  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-ord 6386  df-on 6387

This theorem is referenced by:  epweon  7796  smoiun  8402  dif20el  8544  oeordi  8626  omabs  8690  omsmolem  8696  naddel12  8739  naddsuc2  8740  cofsmo  10310  cfsmolem  10311  inar1  10816  grur1a  10860  nosupno  27749  nosupbnd2lem1  27761  noinfno  27764  noinfbnd2lem1  27776  lrrecpo  27975  addsproplem2  28004  onexoegt  43261  oneltr  43273  oaun3lem1  43392  nadd2rabtr  43402  naddwordnexlem0  43414  oawordex3  43418  naddwordnexlem4  43419