![]() |
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 5957 for more details on why
this definition is desirable. Unlike df-irdg 5957 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 5949 and
tfri2d 5950 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 5919 | . 2 class recs(𝐹) |
3 | vf | . . . . . . . 8 setvar 𝑓 | |
4 | 3 | cv 1242 | . . . . . . 7 class 𝑓 |
5 | vx | . . . . . . . 8 setvar 𝑥 | |
6 | 5 | cv 1242 | . . . . . . 7 class 𝑥 |
7 | 4, 6 | wfn 4897 | . . . . . 6 wff 𝑓 Fn 𝑥 |
8 | vy | . . . . . . . . . 10 setvar 𝑦 | |
9 | 8 | cv 1242 | . . . . . . . . 9 class 𝑦 |
10 | 9, 4 | cfv 4902 | . . . . . . . 8 class (𝑓‘𝑦) |
11 | 4, 9 | cres 4347 | . . . . . . . . 9 class (𝑓 ↾ 𝑦) |
12 | 11, 1 | cfv 4902 | . . . . . . . 8 class (𝐹‘(𝑓 ↾ 𝑦)) |
13 | 10, 12 | wceq 1243 | . . . . . . 7 wff (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) |
14 | 13, 8, 6 | wral 2306 | . . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) |
15 | 7, 14 | wa 97 | . . . . 5 wff (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
16 | con0 4100 | . . . . 5 class On | |
17 | 15, 5, 16 | wrex 2307 | . . . 4 wff ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
18 | 17, 3 | cab 2026 | . . 3 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
19 | 18 | cuni 3580 | . 2 class ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
20 | 2, 19 | wceq 1243 | 1 wff recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
Colors of variables: wff set class |
This definition is referenced by: recseq 5921 nfrecs 5922 recsfval 5931 tfrlem9 5935 tfr0 5937 |
Copyright terms: Public domain | W3C validator |