Metamath Proof Explorer

Theorem nlimsuc

Description: A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024)

Ref Expression
Assertion nlimsuc 
|- ( A e. On -> -. Lim suc A )

Proof

Step Hyp Ref Expression
1 sucidg 
 |-  ( A e. On -> A e. suc A )
2 eloni 
 |-  ( A e. On -> Ord A )
3 ordirr 
 |-  ( Ord A -> -. A e. A )
4 2 3 syl 
 |-  ( A e. On -> -. A e. A )
5 eleq2 
 |-  ( suc A = A -> ( A e. suc A <-> A e. A ) )
6 5 notbid 
 |-  ( suc A = A -> ( -. A e. suc A <-> -. A e. A ) )
7 4 6 syl5ibrcom 
 |-  ( A e. On -> ( suc A = A -> -. A e. suc A ) )
8 1 7 mt2d 
 |-  ( A e. On -> -. suc A = A )
9 8 neqned 
 |-  ( A e. On -> suc A =/= A )
10 onunisuc 
 |-  ( A e. On -> U. suc A = A )
11 9 10 neeqtrrd 
 |-  ( A e. On -> suc A =/= U. suc A )
12 11 neneqd 
 |-  ( A e. On -> -. suc A = U. suc A )
13 12 intn3an3d 
 |-  ( A e. On -> -. ( Ord suc A /\ (/) e. suc A /\ suc A = U. suc A ) )
14 dflim2 
 |-  ( Lim suc A <-> ( Ord suc A /\ (/) e. suc A /\ suc A = U. suc A ) )
15 13 14 sylnibr 
 |-  ( A e. On -> -. Lim suc A )