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

Definition df-recs 5948
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 6013 for more details on why this definition is desirable. Unlike df-irdg 6013 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 5978 and tfri2d 5979 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 5947 . 2 class recs(𝐹)
3 vf . . . . . . . 8 setvar 𝑓
43cv 1284 . . . . . . 7 class 𝑓
5 vx . . . . . . . 8 setvar 𝑥
65cv 1284 . . . . . . 7 class 𝑥
74, 6wfn 4921 . . . . . 6 wff 𝑓 Fn 𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1284 . . . . . . . . 9 class 𝑦
109, 4cfv 4926 . . . . . . . 8 class (𝑓𝑦)
114, 9cres 4367 . . . . . . . . 9 class (𝑓𝑦)
1211, 1cfv 4926 . . . . . . . 8 class (𝐹‘(𝑓𝑦))
1310, 12wceq 1285 . . . . . . 7 wff (𝑓𝑦) = (𝐹‘(𝑓𝑦))
1413, 8, 6wral 2349 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))
157, 14wa 102 . . . . 5 wff (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
16 con0 4120 . . . . 5 class On
1715, 5, 16wrex 2350 . . . 4 wff 𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
1817, 3cab 2068 . . 3 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
1918cuni 3603 . 2 class {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
202, 19wceq 1285 1 wff recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Colors of variables: wff set class
This definition is referenced by:  recseq  5949  nfrecs  5950  recsfval  5958  tfrlem9  5962  tfr0dm  5965  tfr1onlemssrecs  5982  tfrcllemssrecs  5995
  Copyright terms: Public domain W3C validator