Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-recs | GIF version |
Description: Define a function recs(𝐹)
on 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 6235 for more details on why
this definition is desirable. Unlike df-irdg 6235 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 6200 and
tfri2d 6201 for the primary contract of this definition.
(Contributed by Stefan O'Rear, 18-Jan-2015.) |
Ref | Expression |
---|---|
df-recs | ⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cF | . . 3 class 𝐹 | |
2 | 1 | crecs 6169 | . 2 class recs(𝐹) |
3 | vf | . . . . . . . 8 setvar 𝑓 | |
4 | 3 | cv 1315 | . . . . . . 7 class 𝑓 |
5 | vx | . . . . . . . 8 setvar 𝑥 | |
6 | 5 | cv 1315 | . . . . . . 7 class 𝑥 |
7 | 4, 6 | wfn 5088 | . . . . . 6 wff 𝑓 Fn 𝑥 |
8 | vy | . . . . . . . . . 10 setvar 𝑦 | |
9 | 8 | cv 1315 | . . . . . . . . 9 class 𝑦 |
10 | 9, 4 | cfv 5093 | . . . . . . . 8 class (𝑓‘𝑦) |
11 | 4, 9 | cres 4511 | . . . . . . . . 9 class (𝑓 ↾ 𝑦) |
12 | 11, 1 | cfv 5093 | . . . . . . . 8 class (𝐹‘(𝑓 ↾ 𝑦)) |
13 | 10, 12 | wceq 1316 | . . . . . . 7 wff (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) |
14 | 13, 8, 6 | wral 2393 | . . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) |
15 | 7, 14 | wa 103 | . . . . 5 wff (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
16 | con0 4255 | . . . . 5 class On | |
17 | 15, 5, 16 | wrex 2394 | . . . 4 wff ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
18 | 17, 3 | cab 2103 | . . 3 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
19 | 18 | cuni 3706 | . 2 class ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
20 | 2, 19 | wceq 1316 | 1 wff recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
Colors of variables: wff set class |
This definition is referenced by: recseq 6171 nfrecs 6172 recsfval 6180 tfrlem9 6184 tfr0dm 6187 tfr1onlemssrecs 6204 tfrcllemssrecs 6217 |
Copyright terms: Public domain | W3C validator |