Theorem ontr1 6357

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Ord word 6309  Oncon0 6310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-v 3433  df-ss 3900  df-uni 4839  df-tr 5180  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-ord 6313  df-on 6314

This theorem is referenced by:  epweon  7718  smoiun  8291  dif20el  8430  oeordi  8513  omabs  8577  omsmolem  8583  naddel12  8626  naddsuc2  8627  cofsmo  10182  cfsmolem  10183  inar1  10689  grur1a  10733  nosupno  27685  nosupbnd2lem1  27697  noinfno  27700  noinfbnd2lem1  27712  lrrecpo  27951  addsproplem2  27980  r1elcl  35279  onexoegt  43689  oneltr  43701  oaun3lem1  43819  nadd2rabtr  43829  naddwordnexlem0  43841  oawordex3  43845  naddwordnexlem4  43846