Theorem ontr1 6436

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  Ord word 6387  Oncon0 6388

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-ss 3901  df-uni 4873  df-tr 5219  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392

This theorem is used by:  epweon  7821  smoiun  8407  dif20el  8551  oeordi  8634  omabs  8698  omsmolem  8704  naddel12  8748  naddsuc2  8749  cofsmo  10386  cfsmolem  10387  inar1  10899  grur1a  10943  nosupno  28117  nosupbnd2lem1  28129  noinfno  28132  noinfbnd2lem1  28144  lrrecpo  28384  addsproplem2  28413  ontr1i  35830  7olt9o  35915  6olt9o  35916  5olt9o  35917  4olt9o  35918  3olt9o  35919  2olt9o  35920  1olt9o  35921  onexoegt  44507  oneltr  44519  oaun3lem1  44637  nadd2rabtr  44647  naddwordnexlem0  44659  oawordex3  44663  naddwordnexlem4  44664