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 7938
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 7964, wfr2 7965, and wfr3 7966. (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 7937 . 2 class wrecs(𝑅, 𝐴, 𝐹)
5 vf . . . . . . . 8 setvar 𝑓
65cv 1527 . . . . . . 7 class 𝑓
7 vx . . . . . . . 8 setvar 𝑥
87cv 1527 . . . . . . 7 class 𝑥
96, 8wfn 6344 . . . . . 6 wff 𝑓 Fn 𝑥
108, 1wss 3935 . . . . . . 7 wff 𝑥𝐴
11 vy . . . . . . . . . . 11 setvar 𝑦
1211cv 1527 . . . . . . . . . 10 class 𝑦
131, 2, 12cpred 6141 . . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
1413, 8wss 3935 . . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1514, 11, 8wral 3138 . . . . . . 7 wff 𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1610, 15wa 396 . . . . . 6 wff (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
1712, 6cfv 6349 . . . . . . . 8 class (𝑓𝑦)
186, 13cres 5551 . . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
1918, 3cfv 6349 . . . . . . . 8 class (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2017, 19wceq 1528 . . . . . . 7 wff (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2120, 11, 8wral 3138 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
229, 16, 21w3a 1079 . . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2322, 7wex 1771 . . . 4 wff 𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2423, 5cab 2799 . . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2524cuni 4832 . 2 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
264, 25wceq 1528 1 wff wrecs(𝑅, 𝐴, 𝐹) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  wrecseq123  7939  nfwrecs  7940  wfrrel  7951  wfrdmss  7952  wfrdmcl  7954  wfrfun  7956  wfrlem12  7957  wfrlem16  7961  wfrlem17  7962  dfrecs3  8000  csbwrecsg  34491
  Copyright terms: Public domain W3C validator