Theorem eupre2

Description: Unique predecessor exists on the range of the successor map. (Contributed by Peter Mazsa, 12-Jan-2026)

	Ref	Expression
Assertion	eupre2	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ ran SucMap ↔ ∃! 𝑚 𝑚 SucMap 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elrng	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ ran SucMap ↔ ∃ 𝑚 𝑚 SucMap 𝑁 ) )
2		exeupre	⊢ ( 𝑁 ∈ 𝑉 → ( ∃ 𝑚 𝑚 SucMap 𝑁 ↔ ∃! 𝑚 𝑚 SucMap 𝑁 ) )
3	1 2	bitrd	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ ran SucMap ↔ ∃! 𝑚 𝑚 SucMap 𝑁 ) )