| 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 4459). 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 4412 | . 2 class suc 𝐴 |
| 3 | 1 | csn 3633 | . . 3 class {𝐴} |
| 4 | 1, 3 | cun 3164 | . 2 class (𝐴 ∪ {𝐴}) |
| 5 | 2, 4 | wceq 1373 | 1 wff suc 𝐴 = (𝐴 ∪ {𝐴}) |
| Colors of variables: wff set class |
| This definition is referenced by: suceq 4449 elsuci 4450 elsucg 4451 elsuc2g 4452 nfsuc 4455 suc0 4458 sucprc 4459 unisuc 4460 unisucg 4461 sssucid 4462 iunsuc 4467 sucexb 4545 ordsucim 4548 ordsucss 4552 2ordpr 4572 orddif 4595 sucprcreg 4597 elomssom 4653 omsinds 4670 tfrlemisucfn 6410 tfr1onlemsucfn 6426 tfrcllemsucfn 6439 rdgisuc1 6470 df2o3 6516 oasuc 6550 omsuc 6558 enpr2d 6911 phplem1 6949 fiunsnnn 6978 unsnfi 7016 fiintim 7028 fidcenumlemrks 7055 fidcenumlemr 7057 nnnninfeq2 7231 nninfwlpoimlemg 7277 pm54.43 7298 dju1en 7325 pw1nel3 7343 sucpw1nel3 7345 frecfzennn 10571 hashp1i 10955 ennnfonelemg 12774 ennnfonelemhdmp1 12780 ennnfonelemkh 12783 ennnfonelemhf1o 12784 bdcsuc 15816 bdeqsuc 15817 bj-sucexg 15858 bj-nntrans 15887 bj-nnelirr 15889 bj-omtrans 15892 nninfsellemdc 15947 nninfsellemsuc 15949 |
| Copyright terms: Public domain | W3C validator |