Theorem ordtr1 6396

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Tr wtr 5229  Ord word 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-tr 5230  df-ord 6355

This theorem is referenced by:  ontr1  6399  dfsmo2  8361  smores2  8368  smoel  8374  smogt  8381  ordiso2  9529  r1ordg  9792  r1pwss  9798  r1val1  9800  rankr1ai  9812  rankval3b  9840  rankonidlem  9842  onssr1  9845  cofsmo  10283  fpwwe2lem8  10652  nosepssdm  27650  bnj1098  34814  bnj594  34943