Theorem sucmapleftuniq

Description: Left uniqueness of the successor mapping. (Contributed by Peter Mazsa, 8-Jan-2026)

	Ref	Expression
Assertion	sucmapleftuniq	⊢ ( ( 𝐿 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ∧ 𝑁 ∈ 𝑋 ) → ( ( 𝐿 SucMap 𝑁 ∧ 𝑀 SucMap 𝑁 ) → 𝐿 = 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		brsucmap	⊢ ( ( 𝐿 ∈ 𝑉 ∧ 𝑁 ∈ 𝑋 ) → ( 𝐿 SucMap 𝑁 ↔ suc 𝐿 = 𝑁 ) )
2		brsucmap	⊢ ( ( 𝑀 ∈ 𝑊 ∧ 𝑁 ∈ 𝑋 ) → ( 𝑀 SucMap 𝑁 ↔ suc 𝑀 = 𝑁 ) )
3	1 2	bi2anan9	⊢ ( ( ( 𝐿 ∈ 𝑉 ∧ 𝑁 ∈ 𝑋 ) ∧ ( 𝑀 ∈ 𝑊 ∧ 𝑁 ∈ 𝑋 ) ) → ( ( 𝐿 SucMap 𝑁 ∧ 𝑀 SucMap 𝑁 ) ↔ ( suc 𝐿 = 𝑁 ∧ suc 𝑀 = 𝑁 ) ) )
4	3	3impdir	⊢ ( ( 𝐿 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ∧ 𝑁 ∈ 𝑋 ) → ( ( 𝐿 SucMap 𝑁 ∧ 𝑀 SucMap 𝑁 ) ↔ ( suc 𝐿 = 𝑁 ∧ suc 𝑀 = 𝑁 ) ) )
5		eqtr3	⊢ ( ( suc 𝐿 = 𝑁 ∧ suc 𝑀 = 𝑁 ) → suc 𝐿 = suc 𝑀 )
6	4 5	biimtrdi	⊢ ( ( 𝐿 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ∧ 𝑁 ∈ 𝑋 ) → ( ( 𝐿 SucMap 𝑁 ∧ 𝑀 SucMap 𝑁 ) → suc 𝐿 = suc 𝑀 ) )
7		suc11reg	⊢ ( suc 𝐿 = suc 𝑀 ↔ 𝐿 = 𝑀 )
8	6 7	imbitrdi	⊢ ( ( 𝐿 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ∧ 𝑁 ∈ 𝑋 ) → ( ( 𝐿 SucMap 𝑁 ∧ 𝑀 SucMap 𝑁 ) → 𝐿 = 𝑀 ) )