Metamath Proof Explorer

Theorem sucmapleftuniq

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

Ref Expression
Assertion sucmapleftuniq 
|- ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) -> L = M ) )

Proof

Step Hyp Ref Expression
1 brsucmap 
 |-  ( ( L e. V /\ N e. X ) -> ( L SucMap N <-> suc L = N ) )
2 brsucmap 
 |-  ( ( M e. W /\ N e. X ) -> ( M SucMap N <-> suc M = N ) )
3 1 2 bi2anan9 
 |-  ( ( ( L e. V /\ N e. X ) /\ ( M e. W /\ N e. X ) ) -> ( ( L SucMap N /\ M SucMap N ) <-> ( suc L = N /\ suc M = N ) ) )
4 3 3impdir 
 |-  ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) <-> ( suc L = N /\ suc M = N ) ) )
5 eqtr3 
 |-  ( ( suc L = N /\ suc M = N ) -> suc L = suc M )
6 4 5 biimtrdi 
 |-  ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) -> suc L = suc M ) )
7 suc11reg 
 |-  ( suc L = suc M <-> L = M )
8 6 7 imbitrdi 
 |-  ( ( L e. V /\ M e. W /\ N e. X ) -> ( ( L SucMap N /\ M SucMap N ) -> L = M ) )