Theorem ordtr1 6405

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Tr wtr 5218  Ord word 6359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-uni 4873  df-tr 5219  df-ord 6363

This theorem is referenced by:  ontr1  6408  dfsmo2  8330  smores2  8337  smoel  8343  smogt  8350  ordiso2  9473  r1ordg  9746  r1pwss  9752  r1val1  9754  rankr1ai  9766  rankval3b  9794  rankonidlem  9796  onssr1  9799  cofsmo  10248  fpwwe2lem8  10618  nosepssdm  27850  bnj1098  35172  bnj594  35300  rankfilimb  35496  r1filimi  35497