Theorem dfsucmap4

Description: Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	dfsucmap4	⊢ SucMap = ( 𝑚 ∈ V ↦ suc 𝑚 )

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( 𝑛 = suc 𝑚 ↔ suc 𝑚 = 𝑛 )
2	1	opabbii	⊢ { ⟨ 𝑚 , 𝑛 ⟩ ∣ 𝑛 = suc 𝑚 } = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
3		mptv	⊢ ( 𝑚 ∈ V ↦ suc 𝑚 ) = { ⟨ 𝑚 , 𝑛 ⟩ ∣ 𝑛 = suc 𝑚 }
4		df-sucmap	⊢ SucMap = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
5	2 3 4	3eqtr4ri	⊢ SucMap = ( 𝑚 ∈ V ↦ suc 𝑚 )