Theorem dfsuccf2

Description: Alternate definition of Scott Fenton's version of Succ , cf. df-sucmap . (Contributed by Peter Mazsa, 6-Jan-2026)

	Ref	Expression
Assertion	dfsuccf2	$$⊢\mathrm{𝖲𝗎𝖼𝖼}=\left\{⟨m,n⟩|\mathrm{suc}m=n\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-succf	$$⊢\mathrm{𝖲𝗎𝖼𝖼}=\mathrm{𝖢𝗎𝗉}\circ \left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)$$
2		df-co	$$⊢\mathrm{𝖢𝗎𝗉}\circ \left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)=\left\{⟨m,n⟩|\exists x\left(m\left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)x\wedge x\mathrm{𝖢𝗎𝗉}n\right)\right\}$$
3		vex	$$⊢m\in \mathrm{V}$$
4		vex	$$⊢n\in \mathrm{V}$$
5	3 4	lemsuccf	$$⊢\exists x\left(m\left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)x\wedge x\mathrm{𝖢𝗎𝗉}n\right)\leftrightarrow n=\mathrm{suc}m$$
6		eqcom	$$⊢n=\mathrm{suc}m\leftrightarrow \mathrm{suc}m=n$$
7	5 6	bitri	$$⊢\exists x\left(m\left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)x\wedge x\mathrm{𝖢𝗎𝗉}n\right)\leftrightarrow \mathrm{suc}m=n$$
8	7	opabbii	$$⊢\left\{⟨m,n⟩|\exists x\left(m\left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)x\wedge x\mathrm{𝖢𝗎𝗉}n\right)\right\}=\left\{⟨m,n⟩|\mathrm{suc}m=n\right\}$$
9	1 2 8	3eqtri	$$⊢\mathrm{𝖲𝗎𝖼𝖼}=\left\{⟨m,n⟩|\mathrm{suc}m=n\right\}$$