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

Metamath Proof Explorer

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 )