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	$⊢ \neg Lim 2_{𝑜}$

Step	Hyp	Ref	Expression
1		1on	$⊢ 1_{𝑜} \in On$
2		nlimsuc	$⊢ 1_{𝑜} \in On \to \neg Lim suc 1_{𝑜}$
3		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
4		limeq	$⊢ 2_{𝑜} = suc 1_{𝑜} \to (Lim 2_{𝑜} \leftrightarrow Lim suc 1_{𝑜})$
5	3 4	ax-mp	$⊢ Lim 2_{𝑜} \leftrightarrow Lim suc 1_{𝑜}$
6	2 5	sylnibr	$⊢ 1_{𝑜} \in On \to \neg Lim 2_{𝑜}$
7	1 6	ax-mp	$⊢ \neg Lim 2_{𝑜}$

Metamath Proof Explorer