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 4384). 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 4337 | . 2 class suc 𝐴 |
3 | 1 | csn 3570 | . . 3 class {𝐴} |
4 | 1, 3 | cun 3109 | . 2 class (𝐴 ∪ {𝐴}) |
5 | 2, 4 | wceq 1342 | 1 wff suc 𝐴 = (𝐴 ∪ {𝐴}) |
Colors of variables: wff set class |
This definition is referenced by: suceq 4374 elsuci 4375 elsucg 4376 elsuc2g 4377 nfsuc 4380 suc0 4383 sucprc 4384 unisuc 4385 unisucg 4386 sssucid 4387 iunsuc 4392 sucexb 4468 ordsucim 4471 ordsucss 4475 2ordpr 4495 orddif 4518 sucprcreg 4520 elomssom 4576 omsinds 4593 tfrlemisucfn 6283 tfr1onlemsucfn 6299 tfrcllemsucfn 6312 rdgisuc1 6343 df2o3 6389 oasuc 6423 omsuc 6431 enpr2d 6774 phplem1 6809 fiunsnnn 6838 unsnfi 6875 fiintim 6885 fidcenumlemrks 6909 fidcenumlemr 6911 nnnninfeq2 7084 pm54.43 7137 dju1en 7160 pw1nel3 7178 sucpw1nel3 7180 frecfzennn 10351 hashp1i 10712 ennnfonelemg 12279 ennnfonelemhdmp1 12285 ennnfonelemkh 12288 ennnfonelemhf1o 12289 bdcsuc 13603 bdeqsuc 13604 bj-sucexg 13645 bj-nntrans 13674 bj-nnelirr 13676 bj-omtrans 13679 nninfsellemdc 13731 nninfsellemsuc 13733 |
Copyright terms: Public domain | W3C validator |