Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-recs | Unicode version |
Description: Define a function
recs on ,
the class of ordinal
numbers, by transfinite recursion given a rule which sets the next
value given all values so far. See df-irdg 6329 for more details on why
this definition is desirable. Unlike df-irdg 6329 which restricts the
update rule to use only the previous value, this version allows the
update rule to use all previous values, which is why it is
described
as "strong", although it is actually more primitive. See tfri1d 6294 and
tfri2d 6295 for the primary contract of this definition.
(Contributed by Stefan O'Rear, 18-Jan-2015.) |
Ref | Expression |
---|---|
df-recs | recs |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cF | . . 3 | |
2 | 1 | crecs 6263 | . 2 recs |
3 | vf | . . . . . . . 8 | |
4 | 3 | cv 1341 | . . . . . . 7 |
5 | vx | . . . . . . . 8 | |
6 | 5 | cv 1341 | . . . . . . 7 |
7 | 4, 6 | wfn 5177 | . . . . . 6 |
8 | vy | . . . . . . . . . 10 | |
9 | 8 | cv 1341 | . . . . . . . . 9 |
10 | 9, 4 | cfv 5182 | . . . . . . . 8 |
11 | 4, 9 | cres 4600 | . . . . . . . . 9 |
12 | 11, 1 | cfv 5182 | . . . . . . . 8 |
13 | 10, 12 | wceq 1342 | . . . . . . 7 |
14 | 13, 8, 6 | wral 2442 | . . . . . 6 |
15 | 7, 14 | wa 103 | . . . . 5 |
16 | con0 4335 | . . . . 5 | |
17 | 15, 5, 16 | wrex 2443 | . . . 4 |
18 | 17, 3 | cab 2150 | . . 3 |
19 | 18 | cuni 3783 | . 2 |
20 | 2, 19 | wceq 1342 | 1 recs |
Colors of variables: wff set class |
This definition is referenced by: recseq 6265 nfrecs 6266 recsfval 6274 tfrlem9 6278 tfr0dm 6281 tfr1onlemssrecs 6298 tfrcllemssrecs 6311 |
Copyright terms: Public domain | W3C validator |