ordom

Description: Omega is ordinal. Theorem 7.32 of TakeutiZaring p. 43. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	ordom	$⊢ Ord ω$

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 ω$
19		omsson	$⊢ ω \subseteq On$
20		ordon	$⊢ Ord On$
21		trssord	$⊢ (Tr ω \land ω \subseteq On \land Ord On) \to Ord ω$
22	18 19 20 21	mp3an	$⊢ Ord ω$

Metamath Proof Explorer

Theorem ordom

Proof