Definition df-wrecs 8047

Description: Here we define the well-ordered 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 8073, wfr2 8074, and wfr3 8075. (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 8046	. 2 class wrecs(𝑅, 𝐴, 𝐹)
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1542	. . . . . . 7 class 𝑓
7		vx	. . . . . . . 8 setvar 𝑥
8	7	cv 1542	. . . . . . 7 class 𝑥
9	6, 8	wfn 6375	. . . . . 6 wff 𝑓 Fn 𝑥
10	8, 1	wss 3866	. . . . . . 7 wff 𝑥 ⊆ 𝐴
11		vy	. . . . . . . . . . 11 setvar 𝑦
12	11	cv 1542	. . . . . . . . . 10 class 𝑦
13	1, 2, 12	cpred 6159	. . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
14	13, 8	wss 3866	. . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
15	14, 11, 8	wral 3061	. . . . . . 7 wff ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
16	10, 15	wa 399	. . . . . 6 wff (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
17	12, 6	cfv 6380	. . . . . . . 8 class (𝑓‘𝑦)
18	6, 13	cres 5553	. . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
19	18, 3	cfv 6380	. . . . . . . 8 class (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
20	17, 19	wceq 1543	. . . . . . 7 wff (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
21	20, 11, 8	wral 3061	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
22	9, 16, 21	w3a 1089	. . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
23	22, 7	wex 1787	. . . 4 wff ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
24	23, 5	cab 2714	. . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
25	24	cuni 4819	. 2 class ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
26	4, 25	wceq 1543	1 wff wrecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}

This definition is referenced by:  wrecseq123  8048  nfwrecs  8049  wfrrel  8060  wfrdmss  8061  wfrdmcl  8063  wfrfun  8065  wfrlem12  8066  wfrlem16  8070  wfrlem17  8071  dfrecs3  8109  csbwrecsg  35235