Metamath Proof Explorer

Theorem nlim2NEW

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

Ref Expression
Assertion nlim2NEW 
|- -. Lim 2o

Proof

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