Theorem ontr1 6364

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Ord word 6316  Oncon0 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-ss 3918  df-uni 4864  df-tr 5206  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321

This theorem is referenced by:  epweon  7720  smoiun  8293  dif20el  8432  oeordi  8515  omabs  8579  omsmolem  8585  naddel12  8628  naddsuc2  8629  cofsmo  10179  cfsmolem  10180  inar1  10686  grur1a  10730  nosupno  27671  nosupbnd2lem1  27683  noinfno  27686  noinfbnd2lem1  27698  lrrecpo  27937  addsproplem2  27966  r1elcl  35254  onexoegt  43496  oneltr  43508  oaun3lem1  43626  nadd2rabtr  43636  naddwordnexlem0  43648  oawordex3  43652  naddwordnexlem4  43653