Theorem onsucf1o

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

	Ref	Expression
Hypothesis	onsucf1o.f	⊢ 𝐹 = ( 𝑥 ∈ On ↦ suc 𝑥 )
Assertion	onsucf1o	⊢ 𝐹 : On –1-1-onto→ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 }

Proof

Step	Hyp	Ref	Expression
1		onsucf1o.f	⊢ 𝐹 = ( 𝑥 ∈ On ↦ suc 𝑥 )
2	1	fin1a2lem2	⊢ 𝐹 : On –1-1→ On
3		f1fn	⊢ ( 𝐹 : On –1-1→ On → 𝐹 Fn On )
4	2 3	ax-mp	⊢ 𝐹 Fn On
5	1	onsucrn	⊢ ran 𝐹 = { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 }
6	1	fin1a2lem1	⊢ ( 𝑎 ∈ On → ( 𝐹 ‘ 𝑎 ) = suc 𝑎 )
7	1	fin1a2lem1	⊢ ( 𝑏 ∈ On → ( 𝐹 ‘ 𝑏 ) = suc 𝑏 )
8	6 7	eqeqan12d	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ suc 𝑎 = suc 𝑏 ) )
9		suc11	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( suc 𝑎 = suc 𝑏 ↔ 𝑎 = 𝑏 ) )
10	8 9	bitrd	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
11	10	biimpd	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
12	11	rgen2	⊢ ∀ 𝑎 ∈ On ∀ 𝑏 ∈ On ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 )
13		dff1o6	⊢ ( 𝐹 : On –1-1-onto→ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } ↔ ( 𝐹 Fn On ∧ ran 𝐹 = { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } ∧ ∀ 𝑎 ∈ On ∀ 𝑏 ∈ On ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
14	4 5 12 13	mpbir3an	⊢ 𝐹 : On –1-1-onto→ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 }