Definition df-wrecs

Description: Here we define the well-founded recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function F , a relationship R , and a base set A , this definition generates a function G = wrecs ( R , A , F ) that has property that, at any point x e. A , ( Gx ) = ( F` ( G |`Pred ( R , A , x ) ) ) . See wfr1 , wfr2 , and wfr3 . (Contributed by Scott Fenton, 7-Jun-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	df-wrecs	|- wrecs ( 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 ) = ( 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	cwrecs	|- wrecs ( 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	17 2	cfv	|- ( F ` ( f |` Pred ( R , A , y ) ) )
19	16 18	wceq	|- ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
20	19 10 7	wral	|- A. y e. x ( f ` 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
25	3 24	wceq	|- wrecs ( 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 ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }