This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 |-