Definition df-wrecs 7046

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 7072, wfr2 7073, and wfr3 7074. (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 7045	. 2 class wrecs ( R , A , F )
5		vf	. . . . . . . 8 setvar f
6	5	cv 1451	. . . . . . 7 class f
7		vx	. . . . . . . 8 setvar x
8	7	cv 1451	. . . . . . 7 class x
9	6, 8	wfn 5584	. . . . . 6 wff f Fn x
10	8, 1	wss 3390	. . . . . . 7 wff x C_ A
11		vy	. . . . . . . . . . 11 setvar y
12	11	cv 1451	. . . . . . . . . 10 class y
13	1, 2, 12	cpred 5386	. . . . . . . . 9 class Pred ( R , A , y )
14	13, 8	wss 3390	. . . . . . . 8 wff Pred ( R , A , y ) C_ x
15	14, 11, 8	wral 2756	. . . . . . 7 wff A. y e. x Pred ( R , A , y ) C_ x
16	10, 15	wa 376	. . . . . 6 wff ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x )
17	12, 6	cfv 5589	. . . . . . . 8 class ( f ` y )
18	6, 13	cres 4841	. . . . . . . . 9 class ( f |` Pred ( R , A , y ) )
19	18, 3	cfv 5589	. . . . . . . 8 class ( F ` ( f |` Pred ( R , A , y ) ) )
20	17, 19	wceq 1452	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
21	20, 11, 8	wral 2756	. . . . . 6 wff A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
22	9, 16, 21	w3a 1007	. . . . 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 1671	. . . 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 2457	. . 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 4190	. 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 1452	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  7047  nfwrecs  7048  wfrrel  7059  wfrdmss  7060  wfrdmcl  7062  wfrfun  7064  wfrlem12  7065  wfrlem16  7069  wfrlem17  7070  dfrecs3  7109  csbwrecsg  31798