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

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

Metamath Proof Explorer