Theorem ordtr1 6413

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-uni 4870  df-tr 5215  df-ord 6371

This theorem is used by:  ontr1  6416  dfsmo2  8366  smores2  8373  smoel  8379  smogt  8386  ordiso2  9519  r1ordg  9795  r1pwss  9801  r1val1  9803  rankr1ai  9816  rankval3b  9846  rankonidlem  9848  onssr1  9853  r1filimi  9913  cofsmo  10357  fpwwe2lem8  10733  nosepssdm  28055  bnj1098  35467  bnj594  35595  rankfilimb  35789