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

Definition df-wrecs 7574
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 7600, wfr2 7601, and wfr3 7602. (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 7573 . 2 class wrecs(𝑅, 𝐴, 𝐹)
5 vf . . . . . . . 8 setvar 𝑓
65cv 1629 . . . . . . 7 class 𝑓
7 vx . . . . . . . 8 setvar 𝑥
87cv 1629 . . . . . . 7 class 𝑥
96, 8wfn 6042 . . . . . 6 wff 𝑓 Fn 𝑥
108, 1wss 3713 . . . . . . 7 wff 𝑥𝐴
11 vy . . . . . . . . . . 11 setvar 𝑦
1211cv 1629 . . . . . . . . . 10 class 𝑦
131, 2, 12cpred 5838 . . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
1413, 8wss 3713 . . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1514, 11, 8wral 3048 . . . . . . 7 wff 𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1610, 15wa 383 . . . . . 6 wff (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
1712, 6cfv 6047 . . . . . . . 8 class (𝑓𝑦)
186, 13cres 5266 . . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
1918, 3cfv 6047 . . . . . . . 8 class (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2017, 19wceq 1630 . . . . . . 7 wff (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2120, 11, 8wral 3048 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
229, 16, 21w3a 1072 . . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2322, 7wex 1851 . . . 4 wff 𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2423, 5cab 2744 . . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2524cuni 4586 . 2 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
264, 25wceq 1630 1 wff wrecs(𝑅, 𝐴, 𝐹) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  wrecseq123  7575  nfwrecs  7576  wfrrel  7587  wfrdmss  7588  wfrdmcl  7590  wfrfun  7592  wfrlem12  7593  wfrlem16  7597  wfrlem17  7598  dfrecs3  7636  csbwrecsg  33482
  Copyright terms: Public domain W3C validator