![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE 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" (see oa1suc 7200). 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 4958), so that the successor of any ordinal class is still an ordinal class (ordsuc 6649), 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | csuc 4885 | . 2 |
3 | 1 | csn 4029 | . . 3 |
4 | 1, 3 | cun 3473 | . 2 |
5 | 2, 4 | wceq 1395 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: suceq 4948 elsuci 4949 elsucg 4950 elsuc2g 4951 nfsuc 4954 suc0 4957 sucprc 4958 unisuc 4959 sssucid 4960 iunsuc 4965 orddif 4976 sucexb 6644 suceloni 6648 onuninsuci 6675 tfrlem10 7075 tfrlem16 7081 df2o3 7162 oarec 7230 limensuci 7713 infensuc 7715 phplem1 7716 sucdom2 7734 sucxpdom 7749 isinf 7753 pssnn 7758 dif1enOLD 7772 dif1en 7773 fiint 7817 pwfi 7835 dffi3 7911 sucprcreg 8046 sucprcregOLD 8047 cantnfp1lem3 8120 cantnfp1lem3OLD 8146 ranksuc 8304 pm54.43 8402 dif1card 8409 fseqenlem1 8426 cda1en 8576 ackbij1lem1 8621 ackbij1lem2 8622 ackbij1lem5 8625 ackbij1lem14 8634 cfsuc 8658 fin23lem26 8726 axdc3lem4 8854 unsnen 8949 wunsuc 9116 fzennn 12078 hashp1i 12468 dfon2lem3 29217 dfon2lem7 29221 brsuccf 29591 onsucsuccmpi 29908 onint1 29914 pwfi2f1o 31044 sucidALTVD 33670 sucidALT 33671 sucidVD 33672 bnj927 33827 bnj98 33925 bnj543 33951 bnj970 34005 |
Copyright terms: Public domain | W3C validator |