Theorem 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 -> _om C_ A )

Proof

Step	Hyp	Ref	Expression
1		limord	|- ( Lim A -> Ord A )
2		ordeleqon	|- ( Ord A <-> ( A e. On \/ A = On ) )
3		elom	|- ( x e. _om <-> ( x e. On /\ A. y ( Lim y -> x e. y ) ) )
4	3	simprbi	|- ( x e. _om -> A. y ( Lim y -> x e. y ) )
5		limeq	|- ( y = A -> ( Lim y <-> Lim A ) )
6		eleq2	|- ( y = A -> ( x e. y <-> x e. A ) )
7	5 6	imbi12d	|- ( y = A -> ( ( Lim y -> x e. y ) <-> ( Lim A -> x e. A ) ) )
8	7	spcgv	|- ( A e. On -> ( A. y ( Lim y -> x e. y ) -> ( Lim A -> x e. A ) ) )
9	4 8	syl5	|- ( A e. On -> ( x e. _om -> ( Lim A -> x e. A ) ) )
10	9	com23	|- ( A e. On -> ( Lim A -> ( x e. _om -> x e. A ) ) )
11	10	imp	|- ( ( A e. On /\ Lim A ) -> ( x e. _om -> x e. A ) )
12	11	ssrdv	|- ( ( A e. On /\ Lim A ) -> _om C_ A )
13	12	ex	|- ( A e. On -> ( Lim A -> _om C_ A ) )
14		omsson	|- _om C_ On
15		sseq2	|- ( A = On -> ( _om C_ A <-> _om C_ On ) )
16	14 15	mpbiri	|- ( A = On -> _om C_ A )
17	16	a1d	|- ( A = On -> ( Lim A -> _om C_ A ) )
18	13 17	jaoi	|- ( ( A e. On \/ A = On ) -> ( Lim A -> _om C_ A ) )
19	2 18	sylbi	|- ( Ord A -> ( Lim A -> _om C_ A ) )
20	1 19	mpcom	|- ( Lim A -> _om C_ A )