Theorem ontr1 6408

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Ord word 6359  Oncon0 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-ss 3922  df-uni 4873  df-tr 5219  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364

This theorem is referenced by:  epweon  7770  smoiun  8344  dif20el  8486  oeordi  8569  omabs  8633  omsmolem  8639  naddel12  8683  naddsuc2  8684  cofsmo  10248  cfsmolem  10249  inar1  10755  grur1a  10799  nosupno  27867  nosupbnd2lem1  27879  noinfno  27882  noinfbnd2lem1  27894  lrrecpo  28134  addsproplem2  28163  r1elcl  35491  onexoegt  43991  oneltr  44003  oaun3lem1  44121  nadd2rabtr  44131  naddwordnexlem0  44143  oawordex3  44147  naddwordnexlem4  44148