Theorem onsucf1lem

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

	Ref	Expression
Assertion	onsucf1lem	⊢ ( 𝐴 ∈ On → ∃* 𝑏 ∈ On 𝐴 = suc 𝑏 )

Proof

Step	Hyp	Ref	Expression
1		onuni	⊢ ( 𝐴 ∈ On → ∪ 𝐴 ∈ On )
2		onsucuni2	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝑏 ) → suc ∪ 𝐴 = 𝐴 )
3	2	adantlr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝐴 = suc 𝑏 ) → suc ∪ 𝐴 = 𝐴 )
4		simpr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝐴 = suc 𝑏 ) → 𝐴 = suc 𝑏 )
5	3 4	eqtr2d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝐴 = suc 𝑏 ) → suc 𝑏 = suc ∪ 𝐴 )
6	1	anim1i	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) → ( ∪ 𝐴 ∈ On ∧ 𝑏 ∈ On ) )
7	6	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝐴 = suc 𝑏 ) → ( ∪ 𝐴 ∈ On ∧ 𝑏 ∈ On ) )
8	7	ancomd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝐴 = suc 𝑏 ) → ( 𝑏 ∈ On ∧ ∪ 𝐴 ∈ On ) )
9		suc11	⊢ ( ( 𝑏 ∈ On ∧ ∪ 𝐴 ∈ On ) → ( suc 𝑏 = suc ∪ 𝐴 ↔ 𝑏 = ∪ 𝐴 ) )
10	8 9	syl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝐴 = suc 𝑏 ) → ( suc 𝑏 = suc ∪ 𝐴 ↔ 𝑏 = ∪ 𝐴 ) )
11	5 10	mpbid	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) ∧ 𝐴 = suc 𝑏 ) → 𝑏 = ∪ 𝐴 )
12	11	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ On ) → ( 𝐴 = suc 𝑏 → 𝑏 = ∪ 𝐴 ) )
13	12	ralrimiva	⊢ ( 𝐴 ∈ On → ∀ 𝑏 ∈ On ( 𝐴 = suc 𝑏 → 𝑏 = ∪ 𝐴 ) )
14		eqeq2	⊢ ( 𝑐 = ∪ 𝐴 → ( 𝑏 = 𝑐 ↔ 𝑏 = ∪ 𝐴 ) )
15	14	imbi2d	⊢ ( 𝑐 = ∪ 𝐴 → ( ( 𝐴 = suc 𝑏 → 𝑏 = 𝑐 ) ↔ ( 𝐴 = suc 𝑏 → 𝑏 = ∪ 𝐴 ) ) )
16	15	ralbidv	⊢ ( 𝑐 = ∪ 𝐴 → ( ∀ 𝑏 ∈ On ( 𝐴 = suc 𝑏 → 𝑏 = 𝑐 ) ↔ ∀ 𝑏 ∈ On ( 𝐴 = suc 𝑏 → 𝑏 = ∪ 𝐴 ) ) )
17	1 13 16	spcedv	⊢ ( 𝐴 ∈ On → ∃ 𝑐 ∀ 𝑏 ∈ On ( 𝐴 = suc 𝑏 → 𝑏 = 𝑐 ) )
18		nfv	⊢ Ⅎ 𝑐 𝐴 = suc 𝑏
19	18	rmo2	⊢ ( ∃* 𝑏 ∈ On 𝐴 = suc 𝑏 ↔ ∃ 𝑐 ∀ 𝑏 ∈ On ( 𝐴 = suc 𝑏 → 𝑏 = 𝑐 ) )
20	17 19	sylibr	⊢ ( 𝐴 ∈ On → ∃* 𝑏 ∈ On 𝐴 = suc 𝑏 )