Theorem ordtr1 6390

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  Tr wtr 5207  Ord word 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4866  df-tr 5208  df-ord 6349

This theorem is referenced by:  ontr1  6393  dfsmo2  8318  smores2  8325  smoel  8331  smogt  8338  ordiso2  9463  r1ordg  9736  r1pwss  9742  r1val1  9744  rankr1ai  9756  rankval3b  9784  rankonidlem  9786  onssr1  9789  cofsmo  10226  fpwwe2lem8  10596  nosepssdm  27750  bnj1098  35079  bnj594  35207  rankfilimb  35398  r1filimi  35399