Theorem presucmap

Description: pre is really a predecessor (when it should be). This correctness theorem for pre makes it usable in proofs without unfolding iota . This theorem gives one witness; preuniqval gives it is the only one. (Contributed by Peter Mazsa, 12-Jan-2026)

	Ref	Expression
Assertion	presucmap	⊢ ( 𝑁 ∈ ran SucMap → pre 𝑁 SucMap 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		dfpre2	⊢ ( 𝑁 ∈ ran SucMap → pre 𝑁 = ( ℩ 𝑚 𝑚 SucMap 𝑁 ) )
2	1	eqcomd	⊢ ( 𝑁 ∈ ran SucMap → ( ℩ 𝑚 𝑚 SucMap 𝑁 ) = pre 𝑁 )
3		preex	⊢ pre 𝑁 ∈ V
4		eupre2	⊢ ( 𝑁 ∈ ran SucMap → ( 𝑁 ∈ ran SucMap ↔ ∃! 𝑚 𝑚 SucMap 𝑁 ) )
5	4	ibi	⊢ ( 𝑁 ∈ ran SucMap → ∃! 𝑚 𝑚 SucMap 𝑁 )
6		breq1	⊢ ( 𝑚 = pre 𝑁 → ( 𝑚 SucMap 𝑁 ↔ pre 𝑁 SucMap 𝑁 ) )
7	6	iota2	⊢ ( ( pre 𝑁 ∈ V ∧ ∃! 𝑚 𝑚 SucMap 𝑁 ) → ( pre 𝑁 SucMap 𝑁 ↔ ( ℩ 𝑚 𝑚 SucMap 𝑁 ) = pre 𝑁 ) )
8	3 5 7	sylancr	⊢ ( 𝑁 ∈ ran SucMap → ( pre 𝑁 SucMap 𝑁 ↔ ( ℩ 𝑚 𝑚 SucMap 𝑁 ) = pre 𝑁 ) )
9	2 8	mpbird	⊢ ( 𝑁 ∈ ran SucMap → pre 𝑁 SucMap 𝑁 )