Definition df-recs 6596

Description: Define a function recs ( F ) on On, the class of ordinal numbers, by transfinite recursion given a rule F which sets the next value given all values so far. See df-rdg 6631 for more details on why this definition is desirable. Unlike df-rdg 6631 which restricts the update rule to use only the previous value, this version allows the update rule to use all previous values, which is why it is described as "strong", although it is actually more primitive. See recsfnon 6624 and recsval 6625 for the primary contract of this definition.

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7461, zorn2 8346, and dfac8alem 7870. (Contributed by Stefan O'Rear, 18-Jan-2015.) (New usage is discouraged.)

Assertion

Ref	Expression
df-recs	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }

Distinct variable group:   f, F, x, y

Detailed syntax breakdown of Definition df-recs

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2	1	crecs 6595	. 2 class recs ( F )
3		vf	. . . . . . . 8 set f
4	3	cv 1648	. . . . . . 7 class f
5		vx	. . . . . . . 8 set x
6	5	cv 1648	. . . . . . 7 class x
7	4, 6	wfn 5412	. . . . . 6 wff f Fn x
8		vy	. . . . . . . . . 10 set y
9	8	cv 1648	. . . . . . . . 9 class y
10	9, 4	cfv 5417	. . . . . . . 8 class ( f ` y )
11	4, 9	cres 4843	. . . . . . . . 9 class ( f |` y )
12	11, 1	cfv 5417	. . . . . . . 8 class ( F ` ( f |` y ) )
13	10, 12	wceq 1649	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` y ) )
14	13, 8, 6	wral 2670	. . . . . 6 wff A. y e. x ( f ` y ) = ( F ` ( f |` y ) )
15	7, 14	wa 359	. . . . 5 wff ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) )
16		con0 4545	. . . . 5 class On
17	15, 5, 16	wrex 2671	. . . 4 wff E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) )
18	17, 3	cab 2394	. . 3 class { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
19	18	cuni 3979	. 2 class U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
20	2, 19	wceq 1649	1 wff recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }

This definition is referenced by:  recseq  6597  nfrecs  6598  recsfval  6605  tfrlem9  6609  dfrdg2  25370