Metamath Proof Explorer

Theorem trom

Description: The class of finite ordinals _om is a transitive class. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	trom	$⊢ Tr ω$

Proof

Step	Hyp	Ref	Expression
1		dftr2	$⊢ Tr ω \leftrightarrow \forall y \forall x ((y \in x \land x \in ω) \to y \in ω)$
2		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
3	2	expcom	$⊢ y \in x \to (x \in On \to y \in On)$
4		limord	$⊢ Lim z \to Ord z$
5		ordtr	$⊢ Ord z \to Tr z$
6		trel	$⊢ Tr z \to ((y \in x \land x \in z) \to y \in z)$
7	4 5 6	3syl	$⊢ Lim z \to ((y \in x \land x \in z) \to y \in z)$
8	7	expd	$⊢ Lim z \to (y \in x \to (x \in z \to y \in z))$
9	8	com12	$⊢ y \in x \to (Lim z \to (x \in z \to y \in z))$
10	9	a2d	$⊢ y \in x \to ((Lim z \to x \in z) \to (Lim z \to y \in z))$
11	10	alimdv	$⊢ y \in x \to (\forall z (Lim z \to x \in z) \to \forall z (Lim z \to y \in z))$
12	3 11	anim12d	$⊢ y \in x \to ((x \in On \land \forall z (Lim z \to x \in z)) \to (y \in On \land \forall z (Lim z \to y \in z)))$
13		elom	$⊢ x \in ω \leftrightarrow (x \in On \land \forall z (Lim z \to x \in z))$
14		elom	$⊢ y \in ω \leftrightarrow (y \in On \land \forall z (Lim z \to y \in z))$
15	12 13 14	3imtr4g	$⊢ y \in x \to (x \in ω \to y \in ω)$
16	15	imp	$⊢ (y \in x \land x \in ω) \to y \in ω$
17	16	ax-gen	$⊢ \forall x ((y \in x \land x \in ω) \to y \in ω)$
18	1 17	mpgbir	$⊢ Tr ω$