Definition df-frecs 33441

Description: This is the definition for the founded recursion generator. Similar to df-wrecs 7979 and df-recs 8040, it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a founded set-like relationship for its properties, not a well-founded relationship. When this relationship is also a partial ordering, the proof does not use the Axiom of Infinity, but it requires Infinity when the order is not partial. We develop the theorems twice, once with partial ordering and once without. (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 33440	. 2 class frecs(𝑅, 𝐴, 𝐹)
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1541	. . . . . . 7 class 𝑓
7		vx	. . . . . . . 8 setvar 𝑥
8	7	cv 1541	. . . . . . 7 class 𝑥
9	6, 8	wfn 6335	. . . . . 6 wff 𝑓 Fn 𝑥
10	8, 1	wss 3844	. . . . . . 7 wff 𝑥 ⊆ 𝐴
11		vy	. . . . . . . . . . 11 setvar 𝑦
12	11	cv 1541	. . . . . . . . . 10 class 𝑦
13	1, 2, 12	cpred 6129	. . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
14	13, 8	wss 3844	. . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
15	14, 11, 8	wral 3054	. . . . . . 7 wff ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
16	10, 15	wa 399	. . . . . 6 wff (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
17	12, 6	cfv 6340	. . . . . . . 8 class (𝑓‘𝑦)
18	6, 13	cres 5528	. . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
19	12, 18, 3	co 7173	. . . . . . . 8 class (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
20	17, 19	wceq 1542	. . . . . . 7 wff (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
21	20, 11, 8	wral 3054	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
22	9, 16, 21	w3a 1088	. . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
23	22, 7	wex 1786	. . . 4 wff ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
24	23, 5	cab 2717	. . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
25	24	cuni 4797	. 2 class ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
26	4, 25	wceq 1542	1 wff frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}

This definition is referenced by:  frecseq123  33442  nffrecs  33443  frrlem5  33450