Definition df-succf

Description: Define the successor function. See its alternate version dfsuccf2 . See brsuccf for its value. Cf. the equivalent df-sucmap family. (Contributed by Scott Fenton, 14-Apr-2014)

	Ref	Expression
Assertion	df-succf	$$⊢\mathrm{𝖲𝗎𝖼𝖼}=\mathrm{𝖢𝗎𝗉}\circ \left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csuccf	$$class\mathrm{𝖲𝗎𝖼𝖼}$$
1		ccup	$$class\mathrm{𝖢𝗎𝗉}$$
2		cid	$$class\mathrm{I}$$
3		csingle	$$class\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
4	2 3	ctxp	$$class\left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)$$
5	1 4	ccom	$$class\left(\mathrm{𝖢𝗎𝗉}\circ \left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)\right)$$
6	0 5	wceq	$$wff\mathrm{𝖲𝗎𝖼𝖼}=\mathrm{𝖢𝗎𝗉}\circ \left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)$$