Theorem ordtr1

Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004)

	Ref	Expression
Assertion	ordtr1	⊢ ( Ord 𝐶 → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtr	⊢ ( Ord 𝐶 → Tr 𝐶 )
2		trel	⊢ ( Tr 𝐶 → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )
3	1 2	syl	⊢ ( Ord 𝐶 → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )