Theorem ordtr1 6309

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Tr wtr 5191  Ord word 6265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-tr 5192  df-ord 6269

This theorem is referenced by:  ontr1  6312  dfsmo2  8178  smores2  8185  smoel  8191  smogt  8198  ordiso2  9274  r1ordg  9536  r1pwss  9542  r1val1  9544  rankr1ai  9556  rankval3b  9584  rankonidlem  9586  onssr1  9589  cofsmo  10025  fpwwe2lem8  10394  bnj1098  32763  bnj594  32892  nosepssdm  33889