Theorem ontr1 6354

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Ord word 6306  Oncon0 6307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3438  df-ss 3920  df-uni 4859  df-tr 5200  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311

This theorem is referenced by:  epweon  7711  smoiun  8284  dif20el  8423  oeordi  8505  omabs  8569  omsmolem  8575  naddel12  8618  naddsuc2  8619  cofsmo  10163  cfsmolem  10164  inar1  10669  grur1a  10713  nosupno  27613  nosupbnd2lem1  27625  noinfno  27628  noinfbnd2lem1  27640  lrrecpo  27853  addsproplem2  27882  onexoegt  43221  oneltr  43233  oaun3lem1  43351  nadd2rabtr  43361  naddwordnexlem0  43373  oawordex3  43377  naddwordnexlem4  43378