Description: Define the successor function. See brsuccf for its value. (Contributed by Scott Fenton, 14-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-succf | |- Succ = ( Cup o. ( _I (x) Singleton ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | csuccf | |- Succ |
|
1 | ccup | |- Cup |
|
2 | cid | |- _I |
|
3 | csingle | |- Singleton |
|
4 | 2 3 | ctxp | |- ( _I (x) Singleton ) |
5 | 1 4 | ccom | |- ( Cup o. ( _I (x) Singleton ) ) |
6 | 0 5 | wceq | |- Succ = ( Cup o. ( _I (x) Singleton ) ) |