Theorem onsucf1lem

Description: For ordinals, the successor operation is injective, so there is at most one ordinal that a given ordinal could be the succesor of. Lemma 1.17 of Schloeder p. 2. (Contributed by RP, 18-Jan-2025)

	Ref	Expression
Assertion	onsucf1lem	|- ( A e. On -> E* b e. On A = suc b )

Proof

Step	Hyp	Ref	Expression
1		onuni	|- ( A e. On -> U. A e. On )
2		onsucuni2	|- ( ( A e. On /\ A = suc b ) -> suc U. A = A )
3	2	adantlr	|- ( ( ( A e. On /\ b e. On ) /\ A = suc b ) -> suc U. A = A )
4		simpr	|- ( ( ( A e. On /\ b e. On ) /\ A = suc b ) -> A = suc b )
5	3 4	eqtr2d	|- ( ( ( A e. On /\ b e. On ) /\ A = suc b ) -> suc b = suc U. A )
6	1	anim1i	|- ( ( A e. On /\ b e. On ) -> ( U. A e. On /\ b e. On ) )
7	6	adantr	|- ( ( ( A e. On /\ b e. On ) /\ A = suc b ) -> ( U. A e. On /\ b e. On ) )
8	7	ancomd	|- ( ( ( A e. On /\ b e. On ) /\ A = suc b ) -> ( b e. On /\ U. A e. On ) )
9		suc11	|- ( ( b e. On /\ U. A e. On ) -> ( suc b = suc U. A <-> b = U. A ) )
10	8 9	syl	|- ( ( ( A e. On /\ b e. On ) /\ A = suc b ) -> ( suc b = suc U. A <-> b = U. A ) )
11	5 10	mpbid	|- ( ( ( A e. On /\ b e. On ) /\ A = suc b ) -> b = U. A )
12	11	ex	|- ( ( A e. On /\ b e. On ) -> ( A = suc b -> b = U. A ) )
13	12	ralrimiva	|- ( A e. On -> A. b e. On ( A = suc b -> b = U. A ) )
14		eqeq2	|- ( c = U. A -> ( b = c <-> b = U. A ) )
15	14	imbi2d	|- ( c = U. A -> ( ( A = suc b -> b = c ) <-> ( A = suc b -> b = U. A ) ) )
16	15	ralbidv	|- ( c = U. A -> ( A. b e. On ( A = suc b -> b = c ) <-> A. b e. On ( A = suc b -> b = U. A ) ) )
17	1 13 16	spcedv	|- ( A e. On -> E. c A. b e. On ( A = suc b -> b = c ) )
18		nfv	|- F/ c A = suc b
19	18	rmo2	|- ( E* b e. On A = suc b <-> E. c A. b e. On ( A = suc b -> b = c ) )
20	17 19	sylibr	|- ( A e. On -> E* b e. On A = suc b )