Definition df-frecs 33113

Description: This is the definition for the founded recursion generator. Similar to df-wrecs 7941 and df-recs 8002, 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 33112	. 2 class frecs(𝑅, 𝐴, 𝐹)
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1532	. . . . . . 7 class 𝑓
7		vx	. . . . . . . 8 setvar 𝑥
8	7	cv 1532	. . . . . . 7 class 𝑥
9	6, 8	wfn 6344	. . . . . 6 wff 𝑓 Fn 𝑥
10	8, 1	wss 3935	. . . . . . 7 wff 𝑥 ⊆ 𝐴
11		vy	. . . . . . . . . . 11 setvar 𝑦
12	11	cv 1532	. . . . . . . . . 10 class 𝑦
13	1, 2, 12	cpred 6141	. . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
14	13, 8	wss 3935	. . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
15	14, 11, 8	wral 3138	. . . . . . 7 wff ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
16	10, 15	wa 398	. . . . . 6 wff (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
17	12, 6	cfv 6349	. . . . . . . 8 class (𝑓‘𝑦)
18	6, 13	cres 5551	. . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
19	12, 18, 3	co 7150	. . . . . . . 8 class (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
20	17, 19	wceq 1533	. . . . . . 7 wff (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
21	20, 11, 8	wral 3138	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
22	9, 16, 21	w3a 1083	. . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
23	22, 7	wex 1776	. . . 4 wff ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
24	23, 5	cab 2799	. . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
25	24	cuni 4831	. 2 class ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
26	4, 25	wceq 1533	1 wff frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}

This definition is referenced by:  frecseq123  33114  nffrecs  33115  frrlem5  33122