Metamath Proof Explorer

Theorem onsucrn

Description: The successor operation is surjective onto its range, the class of successor ordinals. Lemma 1.17 of Schloeder p. 2. (Contributed by RP, 18-Jan-2025)

		Ref	Expression
	Hypothesis	onsucrn.f	$⊢ F = (x \in On ⟼ suc x)$
	Assertion	onsucrn	$⊢ ran F = \{a \in On \| \exists b \in On a = suc b\}$

Proof

Step	Hyp	Ref	Expression
1		onsucrn.f	$⊢ F = (x \in On ⟼ suc x)$
2		simpr	$⊢ (x \in On \land a = suc x) \to a = suc x$
3		onsuc	$⊢ x \in On \to suc x \in On$
4	3	adantr	$⊢ (x \in On \land a = suc x) \to suc x \in On$
5	2 4	eqeltrd	$⊢ (x \in On \land a = suc x) \to a \in On$
6	5	rexlimiva	$⊢ \exists x \in On a = suc x \to a \in On$
7	6	pm4.71ri	$⊢ \exists x \in On a = suc x \leftrightarrow (a \in On \land \exists x \in On a = suc x)$
8		suceq	$⊢ x = b \to suc x = suc b$
9	8	eqeq2d	$⊢ x = b \to (a = suc x \leftrightarrow a = suc b)$
10	9	cbvrexvw	$⊢ \exists x \in On a = suc x \leftrightarrow \exists b \in On a = suc b$
11	10	anbi2i	$⊢ (a \in On \land \exists x \in On a = suc x) \leftrightarrow (a \in On \land \exists b \in On a = suc b)$
12	7 11	bitri	$⊢ \exists x \in On a = suc x \leftrightarrow (a \in On \land \exists b \in On a = suc b)$
13	12	abbii	$⊢ \{a \| \exists x \in On a = suc x\} = \{a \| (a \in On \land \exists b \in On a = suc b)\}$
14	1	rnmpt	$⊢ ran F = \{a \| \exists x \in On a = suc x\}$
15		df-rab	$⊢ \{a \in On \| \exists b \in On a = suc b\} = \{a \| (a \in On \land \exists b \in On a = suc b)\}$
16	13 14 15	3eqtr4i	$⊢ ran F = \{a \in On \| \exists b \in On a = suc b\}$