tron

Description: The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009)

		Ref	Expression
	Assertion	tron	$⊢ Tr On$

Step	Hyp	Ref	Expression
1		dftr3	$⊢ Tr On \leftrightarrow \forall x \in On x \subseteq On$
2		vex	$⊢ x \in V$
3	2	elon	$⊢ x \in On \leftrightarrow Ord x$
4		ordelord	$⊢ (Ord x \land y \in x) \to Ord y$
5	3 4	sylanb	$⊢ (x \in On \land y \in x) \to Ord y$
6	5	ex	$⊢ x \in On \to (y \in x \to Ord y)$
7		vex	$⊢ y \in V$
8	7	elon	$⊢ y \in On \leftrightarrow Ord y$
9	6 8	imbitrrdi	$⊢ x \in On \to (y \in x \to y \in On)$
10	9	ssrdv	$⊢ x \in On \to x \subseteq On$
11	1 10	mprgbir	$⊢ Tr On$

Metamath Proof Explorer