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 e. On |-> suc x )
Assertion	onsucrn	|- ran F = { a e. On | E. b e. On a = suc b }

Proof

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