This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑁 ) → 𝐿 = 𝑀 ) )