Theorem ordtr1 6350

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Tr wtr 5196  Ord word 6305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857  df-tr 5197  df-ord 6309

This theorem is referenced by:  ontr1  6353  dfsmo2  8267  smores2  8274  smoel  8280  smogt  8287  ordiso2  9401  r1ordg  9671  r1pwss  9677  r1val1  9679  rankr1ai  9691  rankval3b  9719  rankonidlem  9721  onssr1  9724  cofsmo  10160  fpwwe2lem8  10529  nosepssdm  27625  bnj1098  34795  bnj594  34924  rankfilimb  35113  r1filimi  35114