Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-suc | Structured version Visualization version GIF version |
Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7498). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Ordinal natural numbers defined using this successor function and 0 as the empty set are also called von Neumann ordinals; 0 is the empty set {}, 1 is {0, {0}}, 2 is {1, {1}}, and so on. 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 5717), so that the successor of any ordinal class is still an ordinal class (ordsuc 6906), simplifying certain proofs. 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 5642 | . 2 class suc 𝐴 |
3 | 1 | csn 4125 | . . 3 class {𝐴} |
4 | 1, 3 | cun 3538 | . 2 class (𝐴 ∪ {𝐴}) |
5 | 2, 4 | wceq 1475 | 1 wff suc 𝐴 = (𝐴 ∪ {𝐴}) |
Colors of variables: wff setvar class |
This definition is referenced by: suceq 5707 elsuci 5708 elsucg 5709 elsuc2g 5710 nfsuc 5713 suc0 5716 sucprc 5717 unisuc 5718 sssucid 5719 iunsuc 5724 orddif 5737 sucexb 6901 suceloni 6905 onuninsuci 6932 tfrlem10 7370 tfrlem16 7376 df2o3 7460 oarec 7529 limensuci 8021 infensuc 8023 phplem1 8024 sucdom2 8041 sucxpdom 8054 isinf 8058 pssnn 8063 dif1en 8078 fiint 8122 pwfi 8144 dffi3 8220 sucprcreg 8389 cantnfp1lem3 8460 ranksuc 8611 pm54.43 8709 dif1card 8716 fseqenlem1 8730 cda1en 8880 ackbij1lem1 8925 ackbij1lem2 8926 ackbij1lem5 8929 ackbij1lem14 8938 cfsuc 8962 fin23lem26 9030 axdc3lem4 9158 unsnen 9254 wunsuc 9418 fzennn 12629 hashp1i 13052 bnj927 30093 bnj98 30191 bnj543 30217 bnj970 30271 dfon2lem3 30934 dfon2lem7 30938 brsuccf 31218 onsucsuccmpi 31612 onint1 31618 pwfi2f1o 36684 df3o2 37342 df3o3 37343 sucidALTVD 38128 sucidALT 38129 sucidVD 38130 |
Copyright terms: Public domain | W3C validator |