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	⊢ ( 𝑁 ∈ ran SucMap → ∀ 𝑚 ( 𝑚 SucMap 𝑁 → 𝑚 = pre 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		presucmap	⊢ ( 𝑁 ∈ ran SucMap → pre 𝑁 SucMap 𝑁 )
2		preex	⊢ pre 𝑁 ∈ V
3		sucmapleftuniq	⊢ ( ( pre 𝑁 ∈ V ∧ 𝑚 ∈ V ∧ 𝑁 ∈ ran SucMap ) → ( ( pre 𝑁 SucMap 𝑁 ∧ 𝑚 SucMap 𝑁 ) → pre 𝑁 = 𝑚 ) )
4	2 3	mp3an1	⊢ ( ( 𝑚 ∈ V ∧ 𝑁 ∈ ran SucMap ) → ( ( pre 𝑁 SucMap 𝑁 ∧ 𝑚 SucMap 𝑁 ) → pre 𝑁 = 𝑚 ) )
5	4	el2v1	⊢ ( 𝑁 ∈ ran SucMap → ( ( pre 𝑁 SucMap 𝑁 ∧ 𝑚 SucMap 𝑁 ) → pre 𝑁 = 𝑚 ) )
6	1 5	mpand	⊢ ( 𝑁 ∈ ran SucMap → ( 𝑚 SucMap 𝑁 → pre 𝑁 = 𝑚 ) )
7		eqcom	⊢ ( pre 𝑁 = 𝑚 ↔ 𝑚 = pre 𝑁 )
8	6 7	imbitrdi	⊢ ( 𝑁 ∈ ran SucMap → ( 𝑚 SucMap 𝑁 → 𝑚 = pre 𝑁 ) )
9	8	alrimiv	⊢ ( 𝑁 ∈ ran SucMap → ∀ 𝑚 ( 𝑚 SucMap 𝑁 → 𝑚 = pre 𝑁 ) )