Definition df-frecs 8106

Description: This is the definition for the well-founded recursion generator. Similar to df-wrecs 8137 and df-recs 8211, it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a well-founded set-like relationship for its properties, not a well-ordered relationship. This proof requires either a partial order or the axiom of infinity. We develop the theorems twice, once with a partial order and once without. The second development occurs later in the database, after ax-inf 9405 has been introduced. (Contributed by Scott Fenton, 23-Dec-2021.)

Assertion

Ref	Expression
df-frecs	⊢ frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}

Distinct variable groups:   𝑅,𝑓,𝑥,𝑦   𝐴,𝑓,𝑥,𝑦   𝑓,𝐹,𝑥,𝑦

Detailed syntax breakdown of Definition df-frecs

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3		cF	. . 3 class 𝐹
4	1, 2, 3	cfrecs 8105	. 2 class frecs(𝑅, 𝐴, 𝐹)
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1538	. . . . . . 7 class 𝑓
7		vx	. . . . . . . 8 setvar 𝑥
8	7	cv 1538	. . . . . . 7 class 𝑥
9	6, 8	wfn 6432	. . . . . 6 wff 𝑓 Fn 𝑥
10	8, 1	wss 3888	. . . . . . 7 wff 𝑥 ⊆ 𝐴
11		vy	. . . . . . . . . . 11 setvar 𝑦
12	11	cv 1538	. . . . . . . . . 10 class 𝑦
13	1, 2, 12	cpred 6205	. . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
14	13, 8	wss 3888	. . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
15	14, 11, 8	wral 3065	. . . . . . 7 wff ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
16	10, 15	wa 396	. . . . . 6 wff (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
17	12, 6	cfv 6437	. . . . . . . 8 class (𝑓‘𝑦)
18	6, 13	cres 5592	. . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
19	12, 18, 3	co 7284	. . . . . . . 8 class (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
20	17, 19	wceq 1539	. . . . . . 7 wff (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
21	20, 11, 8	wral 3065	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
22	9, 16, 21	w3a 1086	. . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
23	22, 7	wex 1782	. . . 4 wff ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
24	23, 5	cab 2716	. . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
25	24	cuni 4840	. 2 class ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
26	4, 25	wceq 1539	1 wff frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}

This definition is referenced by:  frecseq123  8107  nffrecs  8108  csbfrecsg  8109  frrlem5  8115  fprresex  8135  dfwrecsOLD  8138  dfrecs3  8212