Theorem ordtr1 6402

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 6371	. 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 6356

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213  df-ord 6360

This theorem is used by:  ontr1  6405  dfsmo2  8337  smores2  8344  smoel  8350  smogt  8357  ordiso2  9488  r1ordg  9761  r1pwss  9767  r1val1  9769  rankr1ai  9781  rankval3b  9809  rankonidlem  9811  onssr1  9814  cofsmo  10272  fpwwe2lem8  10648  nosepssdm  27923  bnj1098  35294  bnj594  35422  rankfilimb  35611  r1filimi  35612