Definition df-suc 4889

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.)

Assertion

Ref	Expression
df-suc

Detailed syntax breakdown of Definition 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

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