![]() |
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 4115). 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 4068 |
. 2
![]() ![]() ![]() |
3 | 1 | csn 3367 |
. . 3
![]() ![]() ![]() ![]() |
4 | 1, 3 | cun 2909 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | wceq 1242 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: suceq 4105 elsuci 4106 elsucg 4107 elsuc2g 4108 nfsuc 4111 suc0 4114 sucprc 4115 unisuc 4116 unisucg 4117 sssucid 4118 iunsuc 4123 sucexb 4189 ordsucim 4192 ordsucss 4196 onsucelsucexmidlem 4214 sucprcreg 4227 elnn 4271 tfrlemisucfn 5879 rdgisuc1 5911 df2o3 5953 oasuc 5983 omsuc 5990 frecfzennn 8884 bdcsuc 9335 bdeqsuc 9336 bj-sucexg 9377 bj-nntrans 9411 bj-nnelirr 9413 bj-omtrans 9416 |
Copyright terms: Public domain | W3C validator |