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	$⊢ C \in On \to ((A \in B \land B \in C) \to A \in C)$

Proof

Step	Hyp	Ref	Expression
1		eloni	$⊢ C \in On \to Ord C$
2		ordtr1	$⊢ Ord C \to ((A \in B \land B \in C) \to A \in C)$
3	1 2	syl	$⊢ C \in On \to ((A \in B \land B \in C) \to A \in C)$