Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wrecs Structured version   Visualization version   GIF version

Definition df-wrecs 7452
 Description: Here we define the well-founded recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function 𝐹, a relationship 𝑅, and a base set 𝐴, this definition generates a function 𝐺 = wrecs(𝑅, 𝐴, 𝐹) that has property that, at any point 𝑥 ∈ 𝐴, (𝐺‘𝑥) = (𝐹‘(𝐺 ∣ ‘Pred(𝑅, 𝐴, 𝑥))). See wfr1 7478, wfr2 7479, and wfr3 7480. (Contributed by Scott Fenton, 7-Jun-2018.) (New usage is discouraged.)
Assertion
Ref Expression
df-wrecs wrecs(𝑅, 𝐴, 𝐹) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Distinct variable groups:   𝑅,𝑓,𝑥,𝑦   𝐴,𝑓,𝑥,𝑦   𝑓,𝐹,𝑥,𝑦

Detailed syntax breakdown of Definition df-wrecs
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
3 cF . . 3 class 𝐹
41, 2, 3cwrecs 7451 . 2 class wrecs(𝑅, 𝐴, 𝐹)
5 vf . . . . . . . 8 setvar 𝑓
65cv 1522 . . . . . . 7 class 𝑓
7 vx . . . . . . . 8 setvar 𝑥
87cv 1522 . . . . . . 7 class 𝑥
96, 8wfn 5921 . . . . . 6 wff 𝑓 Fn 𝑥
108, 1wss 3607 . . . . . . 7 wff 𝑥𝐴
11 vy . . . . . . . . . . 11 setvar 𝑦
1211cv 1522 . . . . . . . . . 10 class 𝑦
131, 2, 12cpred 5717 . . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
1413, 8wss 3607 . . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1514, 11, 8wral 2941 . . . . . . 7 wff 𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1610, 15wa 383 . . . . . 6 wff (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
1712, 6cfv 5926 . . . . . . . 8 class (𝑓𝑦)
186, 13cres 5145 . . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
1918, 3cfv 5926 . . . . . . . 8 class (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2017, 19wceq 1523 . . . . . . 7 wff (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2120, 11, 8wral 2941 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
229, 16, 21w3a 1054 . . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2322, 7wex 1744 . . . 4 wff 𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2423, 5cab 2637 . . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2524cuni 4468 . 2 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
264, 25wceq 1523 1 wff wrecs(𝑅, 𝐴, 𝐹) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
 Colors of variables: wff setvar class This definition is referenced by:  wrecseq123  7453  nfwrecs  7454  wfrrel  7465  wfrdmss  7466  wfrdmcl  7468  wfrfun  7470  wfrlem12  7471  wfrlem16  7475  wfrlem17  7476  dfrecs3  7514  csbwrecsg  33303
 Copyright terms: Public domain W3C validator