Theorem nlim4

Description: 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024)

	Ref	Expression
Assertion	nlim4	|- -. Lim 4o

Proof

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