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 ∈ On ⟼ suc ⁡ x
Assertion onsucrn ⊢ ran ⁡ F = a ∈ On | ∃ b ∈ On a = suc ⁡ b

Proof

Step Hyp Ref Expression
1 onsucrn.f ⊢ F = x ∈ On ⟼ suc ⁡ x
2 simpr ⊢ x ∈ On ∧ a = suc ⁡ x → a = suc ⁡ x
3 onsuc ⊢ x ∈ On → suc ⁡ x ∈ On
4 3 adantr ⊢ x ∈ On ∧ a = suc ⁡ x → suc ⁡ x ∈ On
5 2 4 eqeltrd ⊢ x ∈ On ∧ a = suc ⁡ x → a ∈ On
6 5 rexlimiva ⊢ ∃ x ∈ On a = suc ⁡ x → a ∈ On
7 6 pm4.71ri ⊢ ∃ x ∈ On a = suc ⁡ x ↔ a ∈ On ∧ ∃ x ∈ 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 ⊢ ∃ x ∈ On a = suc ⁡ x ↔ ∃ b ∈ On a = suc ⁡ b
11 10 anbi2i ⊢ a ∈ On ∧ ∃ x ∈ On a = suc ⁡ x ↔ a ∈ On ∧ ∃ b ∈ On a = suc ⁡ b
12 7 11 bitri ⊢ ∃ x ∈ On a = suc ⁡ x ↔ a ∈ On ∧ ∃ b ∈ On a = suc ⁡ b
13 12 abbii ⊢ a | ∃ x ∈ On a = suc ⁡ x = a | a ∈ On ∧ ∃ b ∈ On a = suc ⁡ b
14 1 rnmpt ⊢ ran ⁡ F = a | ∃ x ∈ On a = suc ⁡ x
15 df-rab ⊢ a ∈ On | ∃ b ∈ On a = suc ⁡ b = a | a ∈ On ∧ ∃ b ∈ On a = suc ⁡ b
16 13 14 15 3eqtr4i ⊢ ran ⁡ F = a ∈ On | ∃ b ∈ On a = suc ⁡ b