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 ∈ On
2		nlimsuc	⊢ ( 1o ∈ 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 ∈ On → ¬ Lim 2o )
7	1 6	ax-mp	⊢ ¬ Lim 2o