This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ontr1

Description: Transitive law for ordinal numbers. Theorem 7M(b) of Enderton p. 192. Theorem 1.9(ii) of Schloeder p. 1. (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 → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )