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

Metamath Proof Explorer

Theorem nnlim

Description: A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995)

Ref Expression
Assertion nnlim 
|- ( A e. _om -> -. Lim A )

Proof

Step Hyp Ref Expression
1 nnord 
 |-  ( A e. _om -> Ord A )
2 ordirr 
 |-  ( Ord A -> -. A e. A )
3 1 2 syl 
 |-  ( A e. _om -> -. A e. A )
4 elom 
 |-  ( A e. _om <-> ( A e. On /\ A. x ( Lim x -> A e. x ) ) )
5 4 simprbi 
 |-  ( A e. _om -> A. x ( Lim x -> A e. x ) )
6 limeq 
 |-  ( x = A -> ( Lim x <-> Lim A ) )
7 eleq2 
 |-  ( x = A -> ( A e. x <-> A e. A ) )
8 6 7 imbi12d 
 |-  ( x = A -> ( ( Lim x -> A e. x ) <-> ( Lim A -> A e. A ) ) )
9 8 spcgv 
 |-  ( A e. _om -> ( A. x ( Lim x -> A e. x ) -> ( Lim A -> A e. A ) ) )
10 5 9 mpd 
 |-  ( A e. _om -> ( Lim A -> A e. A ) )
11 3 10 mtod 
 |-  ( A e. _om -> -. Lim A )