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 6346 for more details on why
this definition is desirable. Unlike df-irdg 6346 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 6311 and
tfri2d 6312 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 6280 | . 2 class recs(𝐹) |
3 | vf | . . . . . . . 8 setvar 𝑓 | |
4 | 3 | cv 1347 | . . . . . . 7 class 𝑓 |
5 | vx | . . . . . . . 8 setvar 𝑥 | |
6 | 5 | cv 1347 | . . . . . . 7 class 𝑥 |
7 | 4, 6 | wfn 5191 | . . . . . 6 wff 𝑓 Fn 𝑥 |
8 | vy | . . . . . . . . . 10 setvar 𝑦 | |
9 | 8 | cv 1347 | . . . . . . . . 9 class 𝑦 |
10 | 9, 4 | cfv 5196 | . . . . . . . 8 class (𝑓‘𝑦) |
11 | 4, 9 | cres 4611 | . . . . . . . . 9 class (𝑓 ↾ 𝑦) |
12 | 11, 1 | cfv 5196 | . . . . . . . 8 class (𝐹‘(𝑓 ↾ 𝑦)) |
13 | 10, 12 | wceq 1348 | . . . . . . 7 wff (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) |
14 | 13, 8, 6 | wral 2448 | . . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) |
15 | 7, 14 | wa 103 | . . . . 5 wff (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
16 | con0 4346 | . . . . 5 class On | |
17 | 15, 5, 16 | wrex 2449 | . . . 4 wff ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
18 | 17, 3 | cab 2156 | . . 3 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
19 | 18 | cuni 3794 | . 2 class ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
20 | 2, 19 | wceq 1348 | 1 wff recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
Colors of variables: wff set class |
This definition is referenced by: recseq 6282 nfrecs 6283 recsfval 6291 tfrlem9 6295 tfr0dm 6298 tfr1onlemssrecs 6315 tfrcllemssrecs 6328 |
Copyright terms: Public domain | W3C validator |