Theorem nlimsucg

Description: A successor is not a limit ordinal. (Contributed by NM, 25-Mar-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	nlimsucg	|- ( A e. V -> -. Lim suc A )

Proof

Step	Hyp	Ref	Expression
1		limord	|- ( Lim suc A -> Ord suc A )
2		ordsuc	|- ( Ord A <-> Ord suc A )
3	1 2	sylibr	|- ( Lim suc A -> Ord A )
4		limuni	|- ( Lim suc A -> suc A = U. suc A )
5		ordunisuc	|- ( Ord A -> U. suc A = A )
6	5	eqeq2d	|- ( Ord A -> ( suc A = U. suc A <-> suc A = A ) )
7		ordirr	|- ( Ord A -> -. A e. A )
8		eleq2	|- ( suc A = A -> ( A e. suc A <-> A e. A ) )
9	8	notbid	|- ( suc A = A -> ( -. A e. suc A <-> -. A e. A ) )
10	7 9	syl5ibrcom	|- ( Ord A -> ( suc A = A -> -. A e. suc A ) )
11		sucidg	|- ( A e. V -> A e. suc A )
12	11	con3i	|- ( -. A e. suc A -> -. A e. V )
13	10 12	syl6	|- ( Ord A -> ( suc A = A -> -. A e. V ) )
14	6 13	sylbid	|- ( Ord A -> ( suc A = U. suc A -> -. A e. V ) )
15	3 4 14	sylc	|- ( Lim suc A -> -. A e. V )
16	15	con2i	|- ( A e. V -> -. Lim suc A )