Theorem ontr1

Description: Transitive law for ordinal numbers. Theorem 7M(b) of Enderton p. 192. (Contributed by NM, 11-Aug-1994)

	Ref	Expression
Assertion	ontr1	⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐶 ∈ On → Ord 𝐶 )
2		ordtr1	⊢ ( Ord 𝐶 → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )
3	1 2	syl	⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )