Metamath Proof Explorer

Theorem nlim1NEW

Description: 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024) (Proof shortened by RP, 13-Dec-2024)

Ref Expression
Assertion nlim1NEW 
|- -. Lim 1o

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 nlimsuc 
 |-  ( (/) e. On -> -. Lim suc (/) )
3 df-1o 
 |-  1o = suc (/)
4 limeq 
 |-  ( 1o = suc (/) -> ( Lim 1o <-> Lim suc (/) ) )
5 3 4 ax-mp 
 |-  ( Lim 1o <-> Lim suc (/) )
6 2 5 sylnibr 
 |-  ( (/) e. On -> -. Lim 1o )
7 1 6 ax-mp 
 |-  -. Lim 1o