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 )