Definition df-wrecs 7294

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 7320, wfr2 7321, and wfr3 7322. (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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3		cF	. . 3 class 𝐹
4	1, 2, 3	cwrecs 7293	. 2 class wrecs(𝑅, 𝐴, 𝐹)
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1474	. . . . . . 7 class 𝑓
7		vx	. . . . . . . 8 setvar 𝑥
8	7	cv 1474	. . . . . . 7 class 𝑥
9	6, 8	wfn 5799	. . . . . 6 wff 𝑓 Fn 𝑥
10	8, 1	wss 3540	. . . . . . 7 wff 𝑥 ⊆ 𝐴
11		vy	. . . . . . . . . . 11 setvar 𝑦
12	11	cv 1474	. . . . . . . . . 10 class 𝑦
13	1, 2, 12	cpred 5596	. . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
14	13, 8	wss 3540	. . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
15	14, 11, 8	wral 2896	. . . . . . 7 wff ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
16	10, 15	wa 383	. . . . . 6 wff (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
17	12, 6	cfv 5804	. . . . . . . 8 class (𝑓‘𝑦)
18	6, 13	cres 5040	. . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
19	18, 3	cfv 5804	. . . . . . . 8 class (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
20	17, 19	wceq 1475	. . . . . . 7 wff (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
21	20, 11, 8	wral 2896	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
22	9, 16, 21	w3a 1031	. . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
23	22, 7	wex 1695	. . . 4 wff ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
24	23, 5	cab 2596	. . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
25	24	cuni 4372	. 2 class ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
26	4, 25	wceq 1475	1 wff wrecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}

This definition is referenced by:  wrecseq123  7295  nfwrecs  7296  wfrrel  7307  wfrdmss  7308  wfrdmcl  7310  wfrfun  7312  wfrlem12  7313  wfrlem16  7317  wfrlem17  7318  dfrecs3  7356  csbwrecsg  32349