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	|- F = ( x e. On |-> suc x )
Assertion	onsucf1o	|- F : On -1-1-onto-> { a e. On | E. b e. On a = suc b }

Proof

Step	Hyp	Ref	Expression
1		onsucf1o.f	|- F = ( x e. 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 e. On | E. b e. On a = suc b }
6	1	fin1a2lem1	|- ( a e. On -> ( F ` a ) = suc a )
7	1	fin1a2lem1	|- ( b e. On -> ( F ` b ) = suc b )
8	6 7	eqeqan12d	|- ( ( a e. On /\ b e. On ) -> ( ( F ` a ) = ( F ` b ) <-> suc a = suc b ) )
9		suc11	|- ( ( a e. On /\ b e. On ) -> ( suc a = suc b <-> a = b ) )
10	8 9	bitrd	|- ( ( a e. On /\ b e. On ) -> ( ( F ` a ) = ( F ` b ) <-> a = b ) )
11	10	biimpd	|- ( ( a e. On /\ b e. On ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) )
12	11	rgen2	|- A. a e. On A. b e. On ( ( F ` a ) = ( F ` b ) -> a = b )
13		dff1o6	|- ( F : On -1-1-onto-> { a e. On | E. b e. On a = suc b } <-> ( F Fn On /\ ran F = { a e. On | E. b e. On a = suc b } /\ A. a e. On A. b e. On ( ( F ` a ) = ( F ` b ) -> a = b ) ) )
14	4 5 12 13	mpbir3an	|- F : On -1-1-onto-> { a e. On | E. b e. On a = suc b }