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	Could not format assertion : No typesetting found for |- ( N e. ran SucMap -> A. m ( m SucMap N -> m = pre N ) ) with typecode |-

Proof

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