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	⊢ 𝐹 = ( 𝑥 ∈ On ↦ suc 𝑥 )
Assertion	onsucrn	⊢ ran 𝐹 = { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 }

Proof

Step	Hyp	Ref	Expression
1		onsucrn.f	⊢ 𝐹 = ( 𝑥 ∈ On ↦ suc 𝑥 )
2		simpr	⊢ ( ( 𝑥 ∈ On ∧ 𝑎 = suc 𝑥 ) → 𝑎 = suc 𝑥 )
3		onsuc	⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
4	3	adantr	⊢ ( ( 𝑥 ∈ On ∧ 𝑎 = suc 𝑥 ) → suc 𝑥 ∈ On )
5	2 4	eqeltrd	⊢ ( ( 𝑥 ∈ On ∧ 𝑎 = suc 𝑥 ) → 𝑎 ∈ On )
6	5	rexlimiva	⊢ ( ∃ 𝑥 ∈ On 𝑎 = suc 𝑥 → 𝑎 ∈ On )
7	6	pm4.71ri	⊢ ( ∃ 𝑥 ∈ On 𝑎 = suc 𝑥 ↔ ( 𝑎 ∈ On ∧ ∃ 𝑥 ∈ On 𝑎 = suc 𝑥 ) )
8		suceq	⊢ ( 𝑥 = 𝑏 → suc 𝑥 = suc 𝑏 )
9	8	eqeq2d	⊢ ( 𝑥 = 𝑏 → ( 𝑎 = suc 𝑥 ↔ 𝑎 = suc 𝑏 ) )
10	9	cbvrexvw	⊢ ( ∃ 𝑥 ∈ On 𝑎 = suc 𝑥 ↔ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 )
11	10	anbi2i	⊢ ( ( 𝑎 ∈ On ∧ ∃ 𝑥 ∈ On 𝑎 = suc 𝑥 ) ↔ ( 𝑎 ∈ On ∧ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 ) )
12	7 11	bitri	⊢ ( ∃ 𝑥 ∈ On 𝑎 = suc 𝑥 ↔ ( 𝑎 ∈ On ∧ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 ) )
13	12	abbii	⊢ { 𝑎 ∣ ∃ 𝑥 ∈ On 𝑎 = suc 𝑥 } = { 𝑎 ∣ ( 𝑎 ∈ On ∧ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 ) }
14	1	rnmpt	⊢ ran 𝐹 = { 𝑎 ∣ ∃ 𝑥 ∈ On 𝑎 = suc 𝑥 }
15		df-rab	⊢ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } = { 𝑎 ∣ ( 𝑎 ∈ On ∧ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 ) }
16	13 14 15	3eqtr4i	⊢ ran 𝐹 = { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 }