Theorem ontr1 6411

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  Ord word 6364  Oncon0 6365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369

This theorem is referenced by:  epweon  7762  smoiun  8361  dif20el  8505  oeordi  8587  omabs  8650  omsmolem  8656  naddel12  8699  cofsmo  10264  cfsmolem  10265  inar1  10770  grur1a  10814  nosupno  27206  nosupbnd2lem1  27218  noinfno  27221  noinfbnd2lem1  27233  lrrecpo  27425  addsproplem2  27454  onexoegt  41993  oneltr  42005  oaun3lem1  42124  nadd2rabtr  42134  naddsuc2  42143  naddwordnexlem0  42147  oawordex3  42151  naddwordnexlem4  42152