Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-suc | Unicode version |
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4149). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
df-suc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | csuc 4102 | . 2 |
3 | 1 | csn 3375 | . . 3 |
4 | 1, 3 | cun 2915 | . 2 |
5 | 2, 4 | wceq 1243 | 1 |
Colors of variables: wff set class |
This definition is referenced by: suceq 4139 elsuci 4140 elsucg 4141 elsuc2g 4142 nfsuc 4145 suc0 4148 sucprc 4149 unisuc 4150 unisucg 4151 sssucid 4152 iunsuc 4157 sucexb 4223 ordsucim 4226 ordsucss 4230 2ordpr 4249 orddif 4271 sucprcreg 4273 elnn 4328 tfrlemisucfn 5938 rdgisuc1 5971 df2o3 6014 oasuc 6044 omsuc 6051 phplem1 6315 fiunsnnn 6338 frecfzennn 9203 bdcsuc 10000 bdeqsuc 10001 bj-sucexg 10042 bj-nntrans 10076 bj-nnelirr 10078 bj-omtrans 10081 |
Copyright terms: Public domain | W3C validator |