| 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 4458). 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 4411 | . 2 class suc 𝐴 |
| 3 | 1 | csn 3632 | . . 3 class {𝐴} |
| 4 | 1, 3 | cun 3163 | . 2 class (𝐴 ∪ {𝐴}) |
| 5 | 2, 4 | wceq 1372 | 1 wff suc 𝐴 = (𝐴 ∪ {𝐴}) |
| Colors of variables: wff set class |
| This definition is referenced by: suceq 4448 elsuci 4449 elsucg 4450 elsuc2g 4451 nfsuc 4454 suc0 4457 sucprc 4458 unisuc 4459 unisucg 4460 sssucid 4461 iunsuc 4466 sucexb 4544 ordsucim 4547 ordsucss 4551 2ordpr 4571 orddif 4594 sucprcreg 4596 elomssom 4652 omsinds 4669 tfrlemisucfn 6409 tfr1onlemsucfn 6425 tfrcllemsucfn 6438 rdgisuc1 6469 df2o3 6515 oasuc 6549 omsuc 6557 enpr2d 6910 phplem1 6948 fiunsnnn 6977 unsnfi 7015 fiintim 7027 fidcenumlemrks 7054 fidcenumlemr 7056 nnnninfeq2 7230 nninfwlpoimlemg 7276 pm54.43 7297 dju1en 7324 pw1nel3 7342 sucpw1nel3 7344 frecfzennn 10569 hashp1i 10953 ennnfonelemg 12745 ennnfonelemhdmp1 12751 ennnfonelemkh 12754 ennnfonelemhf1o 12755 bdcsuc 15778 bdeqsuc 15779 bj-sucexg 15820 bj-nntrans 15849 bj-nnelirr 15851 bj-omtrans 15854 nninfsellemdc 15909 nninfsellemsuc 15911 |
| Copyright terms: Public domain | W3C validator |