Theorem ordtr1 6369

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866  df-tr 5208  df-ord 6328

This theorem is referenced by:  ontr1  6372  dfsmo2  8289  smores2  8296  smoel  8302  smogt  8309  ordiso2  9432  r1ordg  9702  r1pwss  9708  r1val1  9710  rankr1ai  9722  rankval3b  9750  rankonidlem  9752  onssr1  9755  cofsmo  10191  fpwwe2lem8  10561  nosepssdm  27666  bnj1098  34960  bnj594  35088  rankfilimb  35279  r1filimi  35280