Theorem dfsuccl2

Description: Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 29-Jan-2026)

	Ref	Expression
Assertion	dfsuccl2	Could not format assertion : No typesetting found for |- Suc = { n | E. m suc m = n } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-succl	Could not format Suc = ran SucMap : No typesetting found for |- Suc = ran SucMap with typecode |-
2		df-sucmap	Could not format SucMap = { <. m , n >. | suc m = n } : No typesetting found for |- SucMap = { <. m , n >. | suc m = n } with typecode |-
3	2	rneqi	Could not format ran SucMap = ran { <. m , n >. | suc m = n } : No typesetting found for |- ran SucMap = ran { <. m , n >. | suc m = n } with typecode |-
4		rnopab	$$⊢\mathrm{ran}\left\{⟨m,n⟩|\mathrm{suc}m=n\right\}=\left\{n|\exists m\mathrm{suc}m=n\right\}$$
5	1 3 4	3eqtri	Could not format Suc = { n | E. m suc m = n } : No typesetting found for |- Suc = { n | E. m suc m = n } with typecode |-