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 ( R , A , F ) = U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1		cA	|- A
2		cF	|- F
3	1 0 2	cfrecs	|- frecs ( R , A , F )
4		vf	|- f
5		vx	|- x
6	4	cv	|- f
7	5	cv	|- x
8	6 7	wfn	|- f Fn x
9	7 1	wss	|- x C_ A
10		vy	|- y
11	10	cv	|- y
12	1 0 11	cpred	|- Pred ( R , A , y )
13	12 7	wss	|- Pred ( R , A , y ) C_ x
14	13 10 7	wral	|- A. y e. x Pred ( R , A , y ) C_ x
15	9 14	wa	|- ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x )
16	11 6	cfv	|- ( f ` y )
17	6 12	cres	|- ( f |` Pred ( R , A , y ) )
18	11 17 2	co	|- ( y F ( f |` Pred ( R , A , y ) ) )
19	16 18	wceq	|- ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) )
20	19 10 7	wral	|- A. y e. x ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) )
21	8 15 20	w3a	|- ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) ) )
22	21 5	wex	|- E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) ) )
23	22 4	cab	|- { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) ) ) }
24	23	cuni	|- U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) ) ) }
25	3 24	wceq	|- frecs ( R , A , F ) = U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) ) ) }