limomss

Description: The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of TakeutiZaring p. 44. Remarkably, our proof does not require the Axiom of Infinity. (Contributed by NM, 30-Oct-2003)

		Ref	Expression
	Assertion	limomss	$⊢ Lim A \to ω \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		limord	$⊢ Lim A \to Ord A$
2		ordeleqon	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$
3		elom	$⊢ x \in ω \leftrightarrow (x \in On \land \forall y (Lim y \to x \in y))$
4	3	simprbi	$⊢ x \in ω \to \forall y (Lim y \to x \in y)$
5		limeq	$⊢ y = A \to (Lim y \leftrightarrow Lim A)$
6		eleq2	$⊢ y = A \to (x \in y \leftrightarrow x \in A)$
7	5 6	imbi12d	$⊢ y = A \to ((Lim y \to x \in y) \leftrightarrow (Lim A \to x \in A))$
8	7	spcgv	$⊢ A \in On \to (\forall y (Lim y \to x \in y) \to (Lim A \to x \in A))$
9	4 8	syl5	$⊢ A \in On \to (x \in ω \to (Lim A \to x \in A))$
10	9	com23	$⊢ A \in On \to (Lim A \to (x \in ω \to x \in A))$
11	10	imp	$⊢ (A \in On \land Lim A) \to (x \in ω \to x \in A)$
12	11	ssrdv	$⊢ (A \in On \land Lim A) \to ω \subseteq A$
13	12	ex	$⊢ A \in On \to (Lim A \to ω \subseteq A)$
14		omsson	$⊢ ω \subseteq On$
15		sseq2	$⊢ A = On \to (ω \subseteq A \leftrightarrow ω \subseteq On)$
16	14 15	mpbiri	$⊢ A = On \to ω \subseteq A$
17	16	a1d	$⊢ A = On \to (Lim A \to ω \subseteq A)$
18	13 17	jaoi	$⊢ (A \in On \lor A = On) \to (Lim A \to ω \subseteq A)$
19	2 18	sylbi	$⊢ Ord A \to (Lim A \to ω \subseteq A)$
20	1 19	mpcom	$⊢ Lim A \to ω \subseteq A$

Metamath Proof Explorer

Theorem limomss

Proof