Theorem ordtr1 6216

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2114  Tr wtr 5137  Ord word 6172

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-in 3851  df-ss 3861  df-uni 4798  df-tr 5138  df-ord 6176

This theorem is referenced by:  ontr1  6219  dfsmo2  8016  smores2  8023  smoel  8029  smogt  8036  ordiso2  9055  r1ordg  9283  r1pwss  9289  r1val1  9291  rankr1ai  9303  rankval3b  9331  rankonidlem  9333  onssr1  9336  cofsmo  9772  fpwwe2lem8  10141  bnj1098  32337  bnj594  32466  nosepssdm  33535