Theorem ordtr1 6407

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Tr wtr 5212  Ord word 6361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868  df-tr 5213  df-ord 6365

This theorem is used by:  ontr1  6410  dfsmo2  8355  smores2  8362  smoel  8368  smogt  8375  ordiso2  9509  r1ordg  9785  r1pwss  9791  r1val1  9793  rankr1ai  9806  rankval3b  9836  rankonidlem  9838  onssr1  9843  r1filimi  9903  cofsmo  10347  fpwwe2lem8  10723  nosepssdm  28043  bnj1098  35414  bnj594  35542  rankfilimb  35728