Theorem nlimsuc

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

	Ref	Expression
Assertion	nlimsuc	⊢ ( 𝐴 ∈ On → ¬ Lim suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sucidg	⊢ ( 𝐴 ∈ On → 𝐴 ∈ suc 𝐴 )
2		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
3		ordirr	⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
4	2 3	syl	⊢ ( 𝐴 ∈ On → ¬ 𝐴 ∈ 𝐴 )
5		eleq2	⊢ ( suc 𝐴 = 𝐴 → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ 𝐴 ) )
6	5	notbid	⊢ ( suc 𝐴 = 𝐴 → ( ¬ 𝐴 ∈ suc 𝐴 ↔ ¬ 𝐴 ∈ 𝐴 ) )
7	4 6	syl5ibrcom	⊢ ( 𝐴 ∈ On → ( suc 𝐴 = 𝐴 → ¬ 𝐴 ∈ suc 𝐴 ) )
8	1 7	mt2d	⊢ ( 𝐴 ∈ On → ¬ suc 𝐴 = 𝐴 )
9	8	neqned	⊢ ( 𝐴 ∈ On → suc 𝐴 ≠ 𝐴 )
10		onunisuc	⊢ ( 𝐴 ∈ On → ∪ suc 𝐴 = 𝐴 )
11	9 10	neeqtrrd	⊢ ( 𝐴 ∈ On → suc 𝐴 ≠ ∪ suc 𝐴 )
12	11	neneqd	⊢ ( 𝐴 ∈ On → ¬ suc 𝐴 = ∪ suc 𝐴 )
13	12	intn3an3d	⊢ ( 𝐴 ∈ On → ¬ ( Ord suc 𝐴 ∧ ∅ ∈ suc 𝐴 ∧ suc 𝐴 = ∪ suc 𝐴 ) )
14		dflim2	⊢ ( Lim suc 𝐴 ↔ ( Ord suc 𝐴 ∧ ∅ ∈ suc 𝐴 ∧ suc 𝐴 = ∪ suc 𝐴 ) )
15	13 14	sylnibr	⊢ ( 𝐴 ∈ On → ¬ Lim suc 𝐴 )