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	$$⊢\left(\mathrm{suc}L=N\wedge \mathrm{suc}M=N\right)\to \mathrm{suc}L=\mathrm{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	$$⊢\mathrm{suc}L=\mathrm{suc}M\leftrightarrow 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 |-