Metamath Proof Explorer

Theorem onsucelab

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

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

Proof

Step	Hyp	Ref	Expression
1		onsuc	$⊢ A \in On \to suc A \in On$
2		eqid	$⊢ suc A = suc A$
3		id	$⊢ A \in On \to A \in On$
4		suceq	$⊢ b = A \to suc b = suc A$
5	4	eqeq2d	$⊢ b = A \to (suc A = suc b \leftrightarrow suc A = suc A)$
6	5	adantl	$⊢ (A \in On \land b = A) \to (suc A = suc b \leftrightarrow suc A = suc A)$
7	3 6	rspcedv	$⊢ A \in On \to (suc A = suc A \to \exists b \in On suc A = suc b)$
8	2 7	mpi	$⊢ A \in On \to \exists b \in On suc A = suc b$
9		eqeq1	$⊢ a = suc A \to (a = suc b \leftrightarrow suc A = suc b)$
10	9	rexbidv	$⊢ a = suc A \to (\exists b \in On a = suc b \leftrightarrow \exists b \in On suc A = suc b)$
11	10	elrab	$⊢ suc A \in \{a \in On \| \exists b \in On a = suc b\} \leftrightarrow (suc A \in On \land \exists b \in On suc A = suc b)$
12	1 8 11	sylanbrc	$⊢ A \in On \to suc A \in \{a \in On \| \exists b \in On a = suc b\}$