Theorem nlim3

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

	Ref	Expression
Assertion	nlim3	|- -. Lim 3o

Proof

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