![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-suc | GIF 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 4169). 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 | ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csuc 4122 | . 2 class suc 𝐴 |
3 | 1 | csn 3400 | . . 3 class {𝐴} |
4 | 1, 3 | cun 2972 | . 2 class (𝐴 ∪ {𝐴}) |
5 | 2, 4 | wceq 1285 | 1 wff suc 𝐴 = (𝐴 ∪ {𝐴}) |
Colors of variables: wff set class |
This definition is referenced by: suceq 4159 elsuci 4160 elsucg 4161 elsuc2g 4162 nfsuc 4165 suc0 4168 sucprc 4169 unisuc 4170 unisucg 4171 sssucid 4172 iunsuc 4177 sucexb 4243 ordsucim 4246 ordsucss 4250 2ordpr 4269 orddif 4292 sucprcreg 4294 elnn 4348 tfrlemisucfn 5967 tfr1onlemsucfn 5983 tfrcllemsucfn 5996 rdgisuc1 6027 df2o3 6072 oasuc 6102 omsuc 6109 phplem1 6377 fiunsnnn 6405 unsnfi 6429 pm54.43 6508 frecfzennn 9497 sizep1i 9823 bdcsuc 10814 bdeqsuc 10815 bj-sucexg 10856 bj-nntrans 10889 bj-nnelirr 10891 bj-omtrans 10894 |
Copyright terms: Public domain | W3C validator |