Definition df-wrecs 28913

Description: Here we define the well-founded recursive function generator. This is similar to recs, but works with arbitrary well-founded relationships. (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 28912	. 2 class wrecs ( R , A , F )
5		vf	. . . . . . . 8 setvar f
6	5	cv 1378	. . . . . . 7 class f
7		vx	. . . . . . . 8 setvar x
8	7	cv 1378	. . . . . . 7 class x
9	6, 8	wfn 5581	. . . . . 6 wff f Fn x
10	8, 1	wss 3476	. . . . . . 7 wff x C_ A
11		vy	. . . . . . . . . . 11 setvar y
12	11	cv 1378	. . . . . . . . . 10 class y
13	1, 2, 12	cpred 28820	. . . . . . . . 9 class Pred ( R , A , y )
14	13, 8	wss 3476	. . . . . . . 8 wff Pred ( R , A , y ) C_ x
15	14, 11, 8	wral 2814	. . . . . . 7 wff A. y e. x Pred ( R , A , y ) C_ x
16	10, 15	wa 369	. . . . . 6 wff ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x )
17	12, 6	cfv 5586	. . . . . . . 8 class ( f ` y )
18	6, 13	cres 5001	. . . . . . . . 9 class ( f |` Pred ( R , A , y ) )
19	18, 3	cfv 5586	. . . . . . . 8 class ( F ` ( f |` Pred ( R , A , y ) ) )
20	17, 19	wceq 1379	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
21	20, 11, 8	wral 2814	. . . . . 6 wff A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
22	9, 16, 21	w3a 973	. . . . 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 1596	. . . 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 2452	. . 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 4245	. 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 1379	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  28914  nfwrecs  28915  wfrlem6  28925  wfrlem7  28926  wfrlem9  28928  wfrlem11  28930  wfrlem12  28931  wfrlem16  28935