Theorem ontr1 6404

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Ord word 6356  Oncon0 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-v 3466  df-ss 3948  df-uni 4889  df-tr 5235  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361

This theorem is referenced by:  epweon  7774  smoiun  8380  dif20el  8522  oeordi  8604  omabs  8668  omsmolem  8674  naddel12  8717  naddsuc2  8718  cofsmo  10288  cfsmolem  10289  inar1  10794  grur1a  10838  nosupno  27672  nosupbnd2lem1  27684  noinfno  27687  noinfbnd2lem1  27699  lrrecpo  27905  addsproplem2  27934  onexoegt  43235  oneltr  43247  oaun3lem1  43365  nadd2rabtr  43375  naddwordnexlem0  43387  oawordex3  43391  naddwordnexlem4  43392