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 4334). 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 4287 | . 2 class suc 𝐴 |
3 | 1 | csn 3527 | . . 3 class {𝐴} |
4 | 1, 3 | cun 3069 | . 2 class (𝐴 ∪ {𝐴}) |
5 | 2, 4 | wceq 1331 | 1 wff suc 𝐴 = (𝐴 ∪ {𝐴}) |
Colors of variables: wff set class |
This definition is referenced by: suceq 4324 elsuci 4325 elsucg 4326 elsuc2g 4327 nfsuc 4330 suc0 4333 sucprc 4334 unisuc 4335 unisucg 4336 sssucid 4337 iunsuc 4342 sucexb 4413 ordsucim 4416 ordsucss 4420 2ordpr 4439 orddif 4462 sucprcreg 4464 elnn 4519 omsinds 4535 tfrlemisucfn 6221 tfr1onlemsucfn 6237 tfrcllemsucfn 6250 rdgisuc1 6281 df2o3 6327 oasuc 6360 omsuc 6368 enpr2d 6711 phplem1 6746 fiunsnnn 6775 unsnfi 6807 fiintim 6817 fidcenumlemrks 6841 fidcenumlemr 6843 pm54.43 7046 dju1en 7069 frecfzennn 10199 hashp1i 10556 ennnfonelemg 11916 ennnfonelemhdmp1 11922 ennnfonelemkh 11925 ennnfonelemhf1o 11926 bdcsuc 13078 bdeqsuc 13079 bj-sucexg 13120 bj-nntrans 13149 bj-nnelirr 13151 bj-omtrans 13154 nninfsellemdc 13206 nninfsellemsuc 13208 |
Copyright terms: Public domain | W3C validator |