Theorem ordtr1 6354

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Tr wtr 5179  Ord word 6309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-uni 4839  df-tr 5180  df-ord 6313

This theorem is referenced by:  ontr1  6357  dfsmo2  8277  smores2  8284  smoel  8290  smogt  8297  ordiso2  9420  r1ordg  9693  r1pwss  9699  r1val1  9701  rankr1ai  9713  rankval3b  9741  rankonidlem  9743  onssr1  9746  cofsmo  10182  fpwwe2lem8  10552  nosepssdm  27668  bnj1098  34966  bnj594  35094  rankfilimb  35283  r1filimi  35284