nlimsuc

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

		Ref	Expression
	Assertion	nlimsuc	$⊢ A \in On \to \neg Lim suc A$

Step	Hyp	Ref	Expression
1		sucidg	$⊢ A \in On \to A \in suc A$
2		eloni	$⊢ A \in On \to Ord A$
3		ordirr	$⊢ Ord A \to \neg A \in A$
4	2 3	syl	$⊢ A \in On \to \neg A \in A$
5		eleq2	$⊢ suc A = A \to (A \in suc A \leftrightarrow A \in A)$
6	5	notbid	$⊢ suc A = A \to (\neg A \in suc A \leftrightarrow \neg A \in A)$
7	4 6	syl5ibrcom	$⊢ A \in On \to (suc A = A \to \neg A \in suc A)$
8	1 7	mt2d	$⊢ A \in On \to \neg suc A = A$
9	8	neqned	$⊢ A \in On \to suc A \neq A$
10		onunisuc	$⊢ A \in On \to ⋃ suc A = A$
11	9 10	neeqtrrd	$⊢ A \in On \to suc A \neq ⋃ suc A$
12	11	neneqd	$⊢ A \in On \to \neg suc A = ⋃ suc A$
13	12	intn3an3d	$⊢ A \in On \to \neg (Ord suc A \land \emptyset \in suc A \land suc A = ⋃ suc A)$
14		dflim2	$⊢ Lim suc A \leftrightarrow (Ord suc A \land \emptyset \in suc A \land suc A = ⋃ suc A)$
15	13 14	sylnibr	$⊢ A \in On \to \neg Lim suc A$

Metamath Proof Explorer