Theorem dfsucmap4

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

	Ref	Expression
Assertion	dfsucmap4	Could not format assertion : No typesetting found for |- SucMap = ( m e. _V |-> suc m ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢n=\mathrm{suc}m\leftrightarrow \mathrm{suc}m=n$$
2	1	opabbii	$$⊢\left\{⟨m,n⟩|n=\mathrm{suc}m\right\}=\left\{⟨m,n⟩|\mathrm{suc}m=n\right\}$$
3		mptv	$$⊢\left(m\in \mathrm{V}⟼\mathrm{suc}m\right)=\left\{⟨m,n⟩|n=\mathrm{suc}m\right\}$$
4		df-sucmap	Could not format SucMap = { <. m , n >. | suc m = n } : No typesetting found for |- SucMap = { <. m , n >. | suc m = n } with typecode |-
5	2 3 4	3eqtr4ri	Could not format SucMap = ( m e. _V |-> suc m ) : No typesetting found for |- SucMap = ( m e. _V |-> suc m ) with typecode |-