Theorem ordtr1 6005

Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)

Assertion

Ref	Expression
ordtr1	⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Proof of Theorem ordtr1

Step	Hyp	Ref	Expression
1		ordtr 5976	. 2 ⊢ (Ord 𝐶 → Tr 𝐶)
2		trel 4981	. 2 ⊢ (Tr 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
3	1, 2	syl 17	1 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2166  Tr wtr 4974  Ord word 5961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-v 3415  df-in 3804  df-ss 3811  df-uni 4658  df-tr 4975  df-ord 5965

This theorem is referenced by:  ontr1  6008  dfsmo2  7709  smores2  7716  smoel  7722  smogt  7729  ordiso2  8688  r1ordg  8917  r1pwss  8923  r1val1  8925  rankr1ai  8937  rankval3b  8965  rankonidlem  8967  onssr1  8970  cofsmo  9405  fpwwe2lem9  9774  bnj1098  31399  bnj594  31527  nosepssdm  32374