Theorem ordtr1 6362

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Tr wtr 5193  Ord word 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-tr 5194  df-ord 6321

This theorem is referenced by:  ontr1  6365  dfsmo2  8281  smores2  8288  smoel  8294  smogt  8301  ordiso2  9424  r1ordg  9696  r1pwss  9702  r1val1  9704  rankr1ai  9716  rankval3b  9744  rankonidlem  9746  onssr1  9749  cofsmo  10185  fpwwe2lem8  10555  nosepssdm  27667  bnj1098  34945  bnj594  35073  rankfilimb  35264  r1filimi  35265