Metamath Proof Explorer

Theorem limnsuc

Description: A limit ordinal is not an element of the class of successor ordinals. Definition 1.11 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

		Ref	Expression
	Assertion	limnsuc	$⊢ Lim A \to \neg A \in \{a \in On \| \exists b \in On a = suc b\}$

Proof

Step	Hyp	Ref	Expression
1		dflim6	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land \neg \exists b \in On A = suc b)$
2		simp3	$⊢ (Ord A \land A \neq \emptyset \land \neg \exists b \in On A = suc b) \to \neg \exists b \in On A = suc b$
3		eqeq1	$⊢ a = A \to (a = suc b \leftrightarrow A = suc b)$
4	3	rexbidv	$⊢ a = A \to (\exists b \in On a = suc b \leftrightarrow \exists b \in On A = suc b)$
5	4	elrab	$⊢ A \in \{a \in On \| \exists b \in On a = suc b\} \leftrightarrow (A \in On \land \exists b \in On A = suc b)$
6	5	simprbi	$⊢ A \in \{a \in On \| \exists b \in On a = suc b\} \to \exists b \in On A = suc b$
7	2 6	nsyl	$⊢ (Ord A \land A \neq \emptyset \land \neg \exists b \in On A = suc b) \to \neg A \in \{a \in On \| \exists b \in On a = suc b\}$
8	1 7	sylbi	$⊢ Lim A \to \neg A \in \{a \in On \| \exists b \in On a = suc b\}$