Theorem ordtr1 6367

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Tr wtr 5192  Ord word 6322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851  df-tr 5193  df-ord 6326

This theorem is referenced by:  ontr1  6370  dfsmo2  8287  smores2  8294  smoel  8300  smogt  8307  ordiso2  9430  r1ordg  9702  r1pwss  9708  r1val1  9710  rankr1ai  9722  rankval3b  9750  rankonidlem  9752  onssr1  9755  cofsmo  10191  fpwwe2lem8  10561  nosepssdm  27650  bnj1098  34926  bnj594  35054  rankfilimb  35245  r1filimi  35246