Definition df-succf 36811

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

Assertion

Ref	Expression
df-succf	⊢ Succ = (Cup ∘ ( I ⊗ Singleton))

Detailed syntax breakdown of Definition df-succf

Step	Hyp	Ref	Expression
1		csuccf 36787	. 2 class Succ
2		ccup 36785	. . 3 class Cup
3		cid 5549	. . . 4 class I
4		csingle 36777	. . . 4 class Singleton
5	3, 4	ctxp 36769	. . 3 class ( I ⊗ Singleton)
6	2, 5	ccom 5659	. 2 class (Cup ∘ ( I ⊗ Singleton))
7	1, 6	wceq 1570	1 wff Succ = (Cup ∘ ( I ⊗ Singleton))

This definition is used by:  brsuccf  36881  dfsuccf2  36882