Definition df-wrecs 7407

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, ( G ` x ) = ( F ` ( G | ` Pred ( R , A , x ) ) ). See wfr1 7433, wfr2 7434, and wfr3 7435. (Contributed by Scott Fenton, 7-Jun-2018.) (New usage is discouraged.)

Assertion

Ref	Expression
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 ) ) ) ) }

Distinct variable groups:   R, f, x, y   A, f, x, y   f, F, x, y

Detailed syntax breakdown of Definition df-wrecs

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3		cF	. . 3 class F
4	1, 2, 3	cwrecs 7406	. 2 class wrecs ( R , A , F )
5		vf	. . . . . . . 8 setvar f
6	5	cv 1482	. . . . . . 7 class f
7		vx	. . . . . . . 8 setvar x
8	7	cv 1482	. . . . . . 7 class x
9	6, 8	wfn 5883	. . . . . 6 wff f Fn x
10	8, 1	wss 3574	. . . . . . 7 wff x C_ A
11		vy	. . . . . . . . . . 11 setvar y
12	11	cv 1482	. . . . . . . . . 10 class y
13	1, 2, 12	cpred 5679	. . . . . . . . 9 class Pred ( R , A , y )
14	13, 8	wss 3574	. . . . . . . 8 wff Pred ( R , A , y ) C_ x
15	14, 11, 8	wral 2912	. . . . . . 7 wff A. y e. x Pred ( R , A , y ) C_ x
16	10, 15	wa 384	. . . . . 6 wff ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x )
17	12, 6	cfv 5888	. . . . . . . 8 class ( f ` y )
18	6, 13	cres 5116	. . . . . . . . 9 class ( f |` Pred ( R , A , y ) )
19	18, 3	cfv 5888	. . . . . . . 8 class ( F ` ( f |` Pred ( R , A , y ) ) )
20	17, 19	wceq 1483	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
21	20, 11, 8	wral 2912	. . . . . 6 wff A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
22	9, 16, 21	w3a 1037	. . . . 5 wff ( 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, 7	wex 1704	. . . 4 wff 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, 5	cab 2608	. . 3 class { 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	24	cuni 4436	. 2 class 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 ) ) ) ) }
26	4, 25	wceq 1483	1 wff 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 ) ) ) ) }

This definition is referenced by:  wrecseq123  7408  nfwrecs  7409  wfrrel  7420  wfrdmss  7421  wfrdmcl  7423  wfrfun  7425  wfrlem12  7426  wfrlem16  7430  wfrlem17  7431  dfrecs3  7469  csbwrecsg  33173