nlim4

		Ref	Expression
	Assertion	nlim4	$⊢ \neg Lim 4_{𝑜}$

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

Metamath Proof Explorer