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 6267 for more details on why
this definition is desirable. Unlike df-irdg 6267 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 6232 and
tfri2d 6233 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 6201 | . 2 recs |
3 | vf | . . . . . . . 8 | |
4 | 3 | cv 1330 | . . . . . . 7 |
5 | vx | . . . . . . . 8 | |
6 | 5 | cv 1330 | . . . . . . 7 |
7 | 4, 6 | wfn 5118 | . . . . . 6 |
8 | vy | . . . . . . . . . 10 | |
9 | 8 | cv 1330 | . . . . . . . . 9 |
10 | 9, 4 | cfv 5123 | . . . . . . . 8 |
11 | 4, 9 | cres 4541 | . . . . . . . . 9 |
12 | 11, 1 | cfv 5123 | . . . . . . . 8 |
13 | 10, 12 | wceq 1331 | . . . . . . 7 |
14 | 13, 8, 6 | wral 2416 | . . . . . 6 |
15 | 7, 14 | wa 103 | . . . . 5 |
16 | con0 4285 | . . . . 5 | |
17 | 15, 5, 16 | wrex 2417 | . . . 4 |
18 | 17, 3 | cab 2125 | . . 3 |
19 | 18 | cuni 3736 | . 2 |
20 | 2, 19 | wceq 1331 | 1 recs |
Colors of variables: wff set class |
This definition is referenced by: recseq 6203 nfrecs 6204 recsfval 6212 tfrlem9 6216 tfr0dm 6219 tfr1onlemssrecs 6236 tfrcllemssrecs 6249 |
Copyright terms: Public domain | W3C validator |