Theorem ontr1 6412

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  Ord word 6363  Oncon0 6364

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368

This theorem is used by:  epweon  7780  smoiun  8354  dif20el  8496  oeordi  8579  omabs  8643  omsmolem  8649  naddel12  8693  naddsuc2  8694  cofsmo  10268  cfsmolem  10269  inar1  10777  grur1a  10821  nosupno  27920  nosupbnd2lem1  27932  noinfno  27935  noinfbnd2lem1  27947  lrrecpo  28187  addsproplem2  28216  r1elcl  35551  onexoegt  44031  oneltr  44043  oaun3lem1  44161  nadd2rabtr  44171  naddwordnexlem0  44183  oawordex3  44187  naddwordnexlem4  44188