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	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } )

Proof

Step	Hyp	Ref	Expression
1		onsuc	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
2		eqid	⊢ suc 𝐴 = suc 𝐴
3		id	⊢ ( 𝐴 ∈ On → 𝐴 ∈ On )
4		suceq	⊢ ( 𝑏 = 𝐴 → suc 𝑏 = suc 𝐴 )
5	4	eqeq2d	⊢ ( 𝑏 = 𝐴 → ( suc 𝐴 = suc 𝑏 ↔ suc 𝐴 = suc 𝐴 ) )
6	5	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 = 𝐴 ) → ( suc 𝐴 = suc 𝑏 ↔ suc 𝐴 = suc 𝐴 ) )
7	3 6	rspcedv	⊢ ( 𝐴 ∈ On → ( suc 𝐴 = suc 𝐴 → ∃ 𝑏 ∈ On suc 𝐴 = suc 𝑏 ) )
8	2 7	mpi	⊢ ( 𝐴 ∈ On → ∃ 𝑏 ∈ On suc 𝐴 = suc 𝑏 )
9		eqeq1	⊢ ( 𝑎 = suc 𝐴 → ( 𝑎 = suc 𝑏 ↔ suc 𝐴 = suc 𝑏 ) )
10	9	rexbidv	⊢ ( 𝑎 = suc 𝐴 → ( ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 ↔ ∃ 𝑏 ∈ On suc 𝐴 = suc 𝑏 ) )
11	10	elrab	⊢ ( suc 𝐴 ∈ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } ↔ ( suc 𝐴 ∈ On ∧ ∃ 𝑏 ∈ On suc 𝐴 = suc 𝑏 ) )
12	1 8 11	sylanbrc	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } )