Theorem brsuccf

Description: Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014)

	Ref	Expression
Hypotheses	brsuccf.1	$$⊢A\in \mathrm{V}$$
	brsuccf.2	$$⊢B\in \mathrm{V}$$
Assertion	brsuccf	$$⊢A\mathrm{𝖲𝗎𝖼𝖼}B\leftrightarrow B=\mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		brsuccf.1	$$⊢A\in \mathrm{V}$$
2		brsuccf.2	$$⊢B\in \mathrm{V}$$
3		df-succf	$$⊢\mathrm{𝖲𝗎𝖼𝖼}=\mathrm{𝖢𝗎𝗉}\circ \left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)$$
4	3	breqi	$$⊢A\mathrm{𝖲𝗎𝖼𝖼}B\leftrightarrow A\left(\mathrm{𝖢𝗎𝗉}\circ \left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)\right)B$$
5	1 2	brco	$$⊢A\left(\mathrm{𝖢𝗎𝗉}\circ \left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)\right)B\leftrightarrow \exists x\left(A\left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)x\wedge x\mathrm{𝖢𝗎𝗉}B\right)$$
6	1 2	lemsuccf	$$⊢\exists x\left(A\left(\mathrm{I}\otimes \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)x\wedge x\mathrm{𝖢𝗎𝗉}B\right)\leftrightarrow B=\mathrm{suc}A$$
7	4 5 6	3bitri	$$⊢A\mathrm{𝖲𝗎𝖼𝖼}B\leftrightarrow B=\mathrm{suc}A$$