This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ 𝖲𝗎𝖼𝖼 = 𝖢𝗎𝗉 \circ (I \otimes 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)$

Detailed syntax breakdown

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