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

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

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 6280 . 2 class recs(𝐹)
3 vf . . . . . . . 8 setvar 𝑓
43cv 1347 . . . . . . 7 class 𝑓
5 vx . . . . . . . 8 setvar 𝑥
65cv 1347 . . . . . . 7 class 𝑥
74, 6wfn 5191 . . . . . 6 wff 𝑓 Fn 𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1347 . . . . . . . . 9 class 𝑦
109, 4cfv 5196 . . . . . . . 8 class (𝑓𝑦)
114, 9cres 4611 . . . . . . . . 9 class (𝑓𝑦)
1211, 1cfv 5196 . . . . . . . 8 class (𝐹‘(𝑓𝑦))
1310, 12wceq 1348 . . . . . . 7 wff (𝑓𝑦) = (𝐹‘(𝑓𝑦))
1413, 8, 6wral 2448 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))
157, 14wa 103 . . . . 5 wff (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
16 con0 4346 . . . . 5 class On
1715, 5, 16wrex 2449 . . . 4 wff 𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
1817, 3cab 2156 . . 3 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
1918cuni 3794 . 2 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
202, 19wceq 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