Metamath Proof Explorer

Theorem ontr

Description: An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994) Put in closed form. (Resised by BJ, 28-Dec-2024.)

		Ref	Expression
	Assertion	ontr	$⊢ A \in On \to Tr A$

Step	Hyp	Ref	Expression
1		eloni	$⊢ A \in On \to Ord A$
2		ordtr	$⊢ Ord A \to Tr A$
3	1 2	syl	$⊢ A \in On \to Tr A$