Theorem ordtr1 6406

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  Tr wtr 5222  Ord word 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-uni 4877  df-tr 5223  df-ord 6364

This theorem is referenced by:  ontr1  6409  dfsmo2  8334  smores2  8341  smoel  8347  smogt  8354  ordiso2  9477  r1ordg  9750  r1pwss  9756  r1val1  9758  rankr1ai  9770  rankval3b  9798  rankonidlem  9800  onssr1  9803  cofsmo  10253  fpwwe2lem8  10623  nosepssdm  27816  bnj1098  35117  bnj594  35245  rankfilimb  35438  r1filimi  35439