Metamath Proof Explorer

Theorem onsucf1o

Description: The successor operation is a bijective function between the ordinals and the class of successor ordinals. Lemma 1.17 of Schloeder p. 2. (Contributed by RP, 18-Jan-2025)

Ref Expression
Hypothesis onsucf1o.f ⊢ F = x ∈ On ⟼ suc ⁡ x
Assertion onsucf1o ⊢ F : On ⟶ 1-1 onto a ∈ On | ∃ b ∈ On a = suc ⁡ b

Proof

Step Hyp Ref Expression
1 onsucf1o.f ⊢ F = x ∈ On ⟼ suc ⁡ x
2 1 fin1a2lem2 ⊢ F : On ⟶ 1-1 On
3 f1fn ⊢ F : On ⟶ 1-1 On → F Fn On
4 2 3 ax-mp ⊢ F Fn On
5 1 onsucrn ⊢ ran ⁡ F = a ∈ On | ∃ b ∈ On a = suc ⁡ b
6 1 fin1a2lem1 ⊢ a ∈ On → F ⁡ a = suc ⁡ a
7 1 fin1a2lem1 ⊢ b ∈ On → F ⁡ b = suc ⁡ b
8 6 7 eqeqan12d ⊢ a ∈ On ∧ b ∈ On → F ⁡ a = F ⁡ b ↔ suc ⁡ a = suc ⁡ b
9 suc11 ⊢ a ∈ On ∧ b ∈ On → suc ⁡ a = suc ⁡ b ↔ a = b
10 8 9 bitrd ⊢ a ∈ On ∧ b ∈ On → F ⁡ a = F ⁡ b ↔ a = b
11 10 biimpd ⊢ a ∈ On ∧ b ∈ On → F ⁡ a = F ⁡ b → a = b
12 11 rgen2 ⊢ ∀ a ∈ On ∀ b ∈ On F ⁡ a = F ⁡ b → a = b
13 dff1o6 ⊢ F : On ⟶ 1-1 onto a ∈ On | ∃ b ∈ On a = suc ⁡ b ↔ F Fn On ∧ ran ⁡ F = a ∈ On | ∃ b ∈ On a = suc ⁡ b ∧ ∀ a ∈ On ∀ b ∈ On F ⁡ a = F ⁡ b → a = b
14 4 5 12 13 mpbir3an ⊢ F : On ⟶ 1-1 onto a ∈ On | ∃ b ∈ On a = suc ⁡ b