Definition df-wrecs 27668

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 27667	. 2 class wrecs ( R , A , F )
5		vf	. . . . . . . 8 setvar f
6	5	cv 1368	. . . . . . 7 class f
7		vx	. . . . . . . 8 setvar x
8	7	cv 1368	. . . . . . 7 class x
9	6, 8	wfn 5408	. . . . . 6 wff f Fn x
10	8, 1	wss 3323	. . . . . . 7 wff x C_ A
11		vy	. . . . . . . . . . 11 setvar y
12	11	cv 1368	. . . . . . . . . 10 class y
13	1, 2, 12	cpred 27575	. . . . . . . . 9 class Pred ( R , A , y )
14	13, 8	wss 3323	. . . . . . . 8 wff Pred ( R , A , y ) C_ x
15	14, 11, 8	wral 2710	. . . . . . 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 5413	. . . . . . . 8 class ( f ` y )
18	6, 13	cres 4837	. . . . . . . . 9 class ( f |` Pred ( R , A , y ) )
19	18, 3	cfv 5413	. . . . . . . 8 class ( F ` ( f |` Pred ( R , A , y ) ) )
20	17, 19	wceq 1369	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
21	20, 11, 8	wral 2710	. . . . . 6 wff A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
22	9, 16, 21	w3a 965	. . . . 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 1586	. . . 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 2424	. . 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 4086	. 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 1369	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  27669  nfwrecs  27670  wfrlem6  27680  wfrlem7  27681  wfrlem9  27683  wfrlem11  27685  wfrlem12  27686  wfrlem16  27690