Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-suc | Unicode 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 4304). 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | csuc 4257 | . 2 |
3 | 1 | csn 3497 | . . 3 |
4 | 1, 3 | cun 3039 | . 2 |
5 | 2, 4 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: suceq 4294 elsuci 4295 elsucg 4296 elsuc2g 4297 nfsuc 4300 suc0 4303 sucprc 4304 unisuc 4305 unisucg 4306 sssucid 4307 iunsuc 4312 sucexb 4383 ordsucim 4386 ordsucss 4390 2ordpr 4409 orddif 4432 sucprcreg 4434 elnn 4489 omsinds 4505 tfrlemisucfn 6189 tfr1onlemsucfn 6205 tfrcllemsucfn 6218 rdgisuc1 6249 df2o3 6295 oasuc 6328 omsuc 6336 enpr2d 6679 phplem1 6714 fiunsnnn 6743 unsnfi 6775 fiintim 6785 fidcenumlemrks 6809 fidcenumlemr 6811 pm54.43 7014 dju1en 7037 frecfzennn 10154 hashp1i 10511 ennnfonelemg 11827 ennnfonelemhdmp1 11833 ennnfonelemkh 11836 ennnfonelemhf1o 11837 bdcsuc 12974 bdeqsuc 12975 bj-sucexg 13016 bj-nntrans 13045 bj-nnelirr 13047 bj-omtrans 13050 nninfsellemdc 13102 nninfsellemsuc 13104 |
Copyright terms: Public domain | W3C validator |