Theorem ordtr1 6359

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 6329	. 2 ⊢ (Ord 𝐶 → Tr 𝐶)
2		trel 5211	. 2 ⊢ (Tr 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
3	1, 2	syl 17	1 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Tr wtr 5203  Ord word 6314

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-uni 4862  df-tr 5204  df-ord 6318

This theorem is referenced by:  ontr1  6362  dfsmo2  8277  smores2  8284  smoel  8290  smogt  8297  ordiso2  9418  r1ordg  9688  r1pwss  9694  r1val1  9696  rankr1ai  9708  rankval3b  9736  rankonidlem  9738  onssr1  9741  cofsmo  10177  fpwwe2lem8  10547  nosepssdm  27652  bnj1098  34888  bnj594  35017  rankfilimb  35207  r1filimi  35208