Theorem ontr1 6416

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3455  df-ss 3900  df-uni 4870  df-tr 5215  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  df-ord 6371  df-on 6372

This theorem is used by:  epweon  7796  smoiun  8380  dif20el  8524  oeordi  8607  omabs  8671  omsmolem  8677  naddel12  8721  naddsuc2  8722  cofsmo  10357  cfsmolem  10358  inar1  10870  grur1a  10914  nosupno  28072  nosupbnd2lem1  28084  noinfno  28087  noinfbnd2lem1  28099  lrrecpo  28339  addsproplem2  28368  onexoegt  44386  oneltr  44398  oaun3lem1  44516  nadd2rabtr  44526  naddwordnexlem0  44538  oawordex3  44542  naddwordnexlem4  44543