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 ∈ On
2		nlimsuc	⊢ ( 3o ∈ 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 ∈ On → ¬ Lim 4o )
7	1 6	ax-mp	⊢ ¬ Lim 4o