Definition df-frecs

Description: This is the definition for the well-founded recursion generator. Similar to df-wrecs and df-recs , 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 has been introduced. (Contributed by Scott Fenton, 23-Dec-2021)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2		cF	⊢ 𝐹
3	1 0 2	cfrecs	⊢ frecs ( 𝑅 , 𝐴 , 𝐹 )
4		vf	⊢ 𝑓
5		vx	⊢ 𝑥
6	4	cv	⊢ 𝑓
7	5	cv	⊢ 𝑥
8	6 7	wfn	⊢ 𝑓 Fn 𝑥
9	7 1	wss	⊢ 𝑥 ⊆ 𝐴
10		vy	⊢ 𝑦
11	10	cv	⊢ 𝑦
12	1 0 11	cpred	⊢ Pred ( 𝑅 , 𝐴 , 𝑦 )
13	12 7	wss	⊢ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥
14	13 10 7	wral	⊢ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥
15	9 14	wa	⊢ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 )
16	11 6	cfv	⊢ ( 𝑓 ‘ 𝑦 )
17	6 12	cres	⊢ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) )
18	11 17 2	co	⊢ ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
19	16 18	wceq	⊢ ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
20	19 10 7	wral	⊢ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
21	8 15 20	w3a	⊢ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
22	21 5	wex	⊢ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
23	22 4	cab	⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
24	23	cuni	⊢ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
25	3 24	wceq	⊢ frecs ( 𝑅 , 𝐴 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }