ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-recs GIF version

Definition df-recs 5920
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.)

Assertion
Ref Expression
df-recs recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Distinct variable group:   𝑓,𝐹,𝑥,𝑦

Detailed syntax breakdown of Definition df-recs
StepHypRef Expression
1 cF . . 3 class 𝐹
21crecs 5919 . 2 class recs(𝐹)
3 vf . . . . . . . 8 setvar 𝑓
43cv 1242 . . . . . . 7 class 𝑓
5 vx . . . . . . . 8 setvar 𝑥
65cv 1242 . . . . . . 7 class 𝑥
74, 6wfn 4897 . . . . . 6 wff 𝑓 Fn 𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1242 . . . . . . . . 9 class 𝑦
109, 4cfv 4902 . . . . . . . 8 class (𝑓𝑦)
114, 9cres 4347 . . . . . . . . 9 class (𝑓𝑦)
1211, 1cfv 4902 . . . . . . . 8 class (𝐹‘(𝑓𝑦))
1310, 12wceq 1243 . . . . . . 7 wff (𝑓𝑦) = (𝐹‘(𝑓𝑦))
1413, 8, 6wral 2306 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))
157, 14wa 97 . . . . 5 wff (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
16 con0 4100 . . . . 5 class On
1715, 5, 16wrex 2307 . . . 4 wff 𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
1817, 3cab 2026 . . 3 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
1918cuni 3580 . 2 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
202, 19wceq 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