Theorem onsucelab

Description: The successor of every ordinal is an element of the class of successor ordinals. Definition 1.11 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

	Ref	Expression
Assertion	onsucelab	|- ( A e. On -> suc A e. { a e. On | E. b e. On a = suc b } )

Proof

Step	Hyp	Ref	Expression
1		onsuc	|- ( A e. On -> suc A e. On )
2		eqid	|- suc A = suc A
3		id	|- ( A e. On -> A e. On )
4		suceq	|- ( b = A -> suc b = suc A )
5	4	eqeq2d	|- ( b = A -> ( suc A = suc b <-> suc A = suc A ) )
6	5	adantl	|- ( ( A e. On /\ b = A ) -> ( suc A = suc b <-> suc A = suc A ) )
7	3 6	rspcedv	|- ( A e. On -> ( suc A = suc A -> E. b e. On suc A = suc b ) )
8	2 7	mpi	|- ( A e. On -> E. b e. On suc A = suc b )
9		eqeq1	|- ( a = suc A -> ( a = suc b <-> suc A = suc b ) )
10	9	rexbidv	|- ( a = suc A -> ( E. b e. On a = suc b <-> E. b e. On suc A = suc b ) )
11	10	elrab	|- ( suc A e. { a e. On | E. b e. On a = suc b } <-> ( suc A e. On /\ E. b e. On suc A = suc b ) )
12	1 8 11	sylanbrc	|- ( A e. On -> suc A e. { a e. On | E. b e. On a = suc b } )