limom

Description: Omega is a limit ordinal. Theorem 2.8 of BellMachover p. 473. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995) (Proof shortened by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	limom	$⊢ Lim ω$

Proof

Step	Hyp	Ref	Expression
1		ordom	$⊢ Ord ω$
2		ordeleqon	$⊢ Ord ω \leftrightarrow (ω \in On \lor ω = On)$
3		ordirr	$⊢ Ord ω \to \neg ω \in ω$
4	1 3	ax-mp	$⊢ \neg ω \in ω$
5		elom	$⊢ ω \in ω \leftrightarrow (ω \in On \land \forall x (Lim x \to ω \in x))$
6	5	baib	$⊢ ω \in On \to (ω \in ω \leftrightarrow \forall x (Lim x \to ω \in x))$
7	4 6	mtbii	$⊢ ω \in On \to \neg \forall x (Lim x \to ω \in x)$
8		limomss	$⊢ Lim x \to ω \subseteq x$
9		limord	$⊢ Lim x \to Ord x$
10		ordsseleq	$⊢ (Ord ω \land Ord x) \to (ω \subseteq x \leftrightarrow (ω \in x \lor ω = x))$
11	1 9 10	sylancr	$⊢ Lim x \to (ω \subseteq x \leftrightarrow (ω \in x \lor ω = x))$
12	8 11	mpbid	$⊢ Lim x \to (ω \in x \lor ω = x)$
13	12	ord	$⊢ Lim x \to (\neg ω \in x \to ω = x)$
14		limeq	$⊢ ω = x \to (Lim ω \leftrightarrow Lim x)$
15	14	biimprcd	$⊢ Lim x \to (ω = x \to Lim ω)$
16	13 15	syld	$⊢ Lim x \to (\neg ω \in x \to Lim ω)$
17	16	con1d	$⊢ Lim x \to (\neg Lim ω \to ω \in x)$
18	17	com12	$⊢ \neg Lim ω \to (Lim x \to ω \in x)$
19	18	alrimiv	$⊢ \neg Lim ω \to \forall x (Lim x \to ω \in x)$
20	7 19	nsyl2	$⊢ ω \in On \to Lim ω$
21		limon	$⊢ Lim On$
22		limeq	$⊢ ω = On \to (Lim ω \leftrightarrow Lim On)$
23	21 22	mpbiri	$⊢ ω = On \to Lim ω$
24	20 23	jaoi	$⊢ (ω \in On \lor ω = On) \to Lim ω$
25	2 24	sylbi	$⊢ Ord ω \to Lim ω$
26	1 25	ax-mp	$⊢ Lim ω$

Metamath Proof Explorer

Theorem limom

Proof