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 Could not format assertion : No typesetting found for |- ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) -> L = M ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 brsucmap Could not format ( ( L e. V /\ N e. X ) -> ( L SucMap N <-> suc L = N ) ) : No typesetting found for |- ( ( L e. V /\ N e. X ) -> ( L SucMap N <-> suc L = N ) ) with typecode |-
2 brsucmap Could not format ( ( M e. W /\ N e. X ) -> ( M SucMap N <-> suc M = N ) ) : No typesetting found for |- ( ( M e. W /\ N e. X ) -> ( M SucMap N <-> suc M = N ) ) with typecode |-
3 1 2 bi2anan9 Could not format ( ( ( L e. V /\ N e. X ) /\ ( M e. W /\ N e. X ) ) -> ( ( L SucMap N /\ M SucMap N ) <-> ( suc L = N /\ suc M = N ) ) ) : No typesetting found for |- ( ( ( L e. V /\ N e. X ) /\ ( M e. W /\ N e. X ) ) -> ( ( L SucMap N /\ M SucMap N ) <-> ( suc L = N /\ suc M = N ) ) ) with typecode |-
4 3 3impdir Could not format ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) <-> ( suc L = N /\ suc M = N ) ) ) : No typesetting found for |- ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) <-> ( suc L = N /\ suc M = N ) ) ) with typecode |-
5 eqtr3 ⊢ suc ⁡ L = N ∧ suc ⁡ M = N → suc ⁡ L = suc ⁡ M
6 4 5 biimtrdi Could not format ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) -> suc L = suc M ) ) : No typesetting found for |- ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) -> suc L = suc M ) ) with typecode |-
7 suc11reg ⊢ suc ⁡ L = suc ⁡ M ↔ L = M
8 6 7 imbitrdi Could not format ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) -> L = M ) ) : No typesetting found for |- ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) -> L = M ) ) with typecode |-