This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )