Metamath Proof Explorer

Theorem preuniqval

Description: Uniqueness/canonicity of pre . presucmap gives one witness; this theorem gives it is the only one. It turns any predecessor proof into an equality with pre N . (Contributed by Peter Mazsa, 12-Jan-2026)

Ref Expression
Assertion preuniqval 
|- ( N e. ran SucMap -> A. m ( m SucMap N -> m = pre N ) )

Proof

Step Hyp Ref Expression
1 presucmap 
 |-  ( N e. ran SucMap -> pre N SucMap N )
2 preex 
 |-  pre N e. _V
3 sucmapleftuniq 
 |-  ( ( pre N e. _V /\ m e. _V /\ N e. ran SucMap ) -> ( ( pre N SucMap N /\ m SucMap N ) -> pre N = m ) )
4 2 3 mp3an1 
 |-  ( ( m e. _V /\ N e. ran SucMap ) -> ( ( pre N SucMap N /\ m SucMap N ) -> pre N = m ) )
5 4 el2v1 
 |-  ( N e. ran SucMap -> ( ( pre N SucMap N /\ m SucMap N ) -> pre N = m ) )
6 1 5 mpand 
 |-  ( N e. ran SucMap -> ( m SucMap N -> pre N = m ) )
7 eqcom 
 |-  ( pre N = m <-> m = pre N )
8 6 7 imbitrdi 
 |-  ( N e. ran SucMap -> ( m SucMap N -> m = pre N ) )
9 8 alrimiv 
 |-  ( N e. ran SucMap -> A. m ( m SucMap N -> m = pre N ) )