Theorem ordtr1 6409

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  Tr wtr 5220  Ord word 6363

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221  df-ord 6367

This theorem is used by:  ontr1  6412  dfsmo2  8340  smores2  8347  smoel  8353  smogt  8360  ordiso2  9484  r1ordg  9757  r1pwss  9763  r1val1  9765  rankr1ai  9777  rankval3b  9805  rankonidlem  9807  onssr1  9810  cofsmo  10268  fpwwe2lem8  10640  nosepssdm  27903  bnj1098  35239  bnj594  35367  rankfilimb  35556  r1filimi  35557