Theorem ontr1 6405

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Ord word 6356  Oncon0 6357

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361

This theorem is used by:  epweon  7775  smoiun  8351  dif20el  8493  oeordi  8576  omabs  8640  omsmolem  8646  naddel12  8690  naddsuc2  8691  cofsmo  10272  cfsmolem  10273  inar1  10785  grur1a  10829  nosupno  27940  nosupbnd2lem1  27952  noinfno  27955  noinfbnd2lem1  27967  lrrecpo  28207  addsproplem2  28236  r1elcl  35606  onexoegt  44086  oneltr  44098  oaun3lem1  44216  nadd2rabtr  44226  naddwordnexlem0  44238  oawordex3  44242  naddwordnexlem4  44243