Theorem ordtr1 6364

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Tr wtr 5209  Ord word 6319

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868  df-tr 5210  df-ord 6323

This theorem is referenced by:  ontr1  6367  dfsmo2  8293  smores2  8300  smoel  8306  smogt  8313  ordiso2  9444  r1ordg  9707  r1pwss  9713  r1val1  9715  rankr1ai  9727  rankval3b  9755  rankonidlem  9757  onssr1  9760  cofsmo  10198  fpwwe2lem8  10567  nosepssdm  27574  bnj1098  34746  bnj594  34875