Definition df-wrecs 7027

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 7053, wfr2 7054, and wfr3 7055. (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 7026	. 2 class wrecs ( R , A , F )
5		vf	. . . . . . . 8 setvar f
6	5	cv 1436	. . . . . . 7 class f
7		vx	. . . . . . . 8 setvar x
8	7	cv 1436	. . . . . . 7 class x
9	6, 8	wfn 5587	. . . . . 6 wff f Fn x
10	8, 1	wss 3433	. . . . . . 7 wff x C_ A
11		vy	. . . . . . . . . . 11 setvar y
12	11	cv 1436	. . . . . . . . . 10 class y
13	1, 2, 12	cpred 5389	. . . . . . . . 9 class Pred ( R , A , y )
14	13, 8	wss 3433	. . . . . . . 8 wff Pred ( R , A , y ) C_ x
15	14, 11, 8	wral 2773	. . . . . . 7 wff A. y e. x Pred ( R , A , y ) C_ x
16	10, 15	wa 370	. . . . . 6 wff ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x )
17	12, 6	cfv 5592	. . . . . . . 8 class ( f ` y )
18	6, 13	cres 4847	. . . . . . . . 9 class ( f |` Pred ( R , A , y ) )
19	18, 3	cfv 5592	. . . . . . . 8 class ( F ` ( f |` Pred ( R , A , y ) ) )
20	17, 19	wceq 1437	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
21	20, 11, 8	wral 2773	. . . . . 6 wff A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
22	9, 16, 21	w3a 982	. . . . 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 1659	. . . 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 2405	. . 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 4213	. 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 1437	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  7028  nfwrecs  7029  wfrrel  7040  wfrdmss  7041  wfrdmcl  7043  wfrfun  7045  wfrlem12  7046  wfrlem16  7050  wfrlem17  7051  dfrecs3  7090