Definition df-recs 6342

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 6377 for more details on why this definition is desirable. Unlike df-rdg 6377 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 6370 and recsval 6371 for the primary contract of this definition.

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7201, zorn2 8087, and dfac8alem 7610. (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 6341	. 2 class recs ( F )
3		vf	. . . . . . . 8 set f
4	3	cv 1618	. . . . . . 7 class f
5		vx	. . . . . . . 8 set x
6	5	cv 1618	. . . . . . 7 class x
7	4, 6	wfn 4654	. . . . . 6 wff f Fn x
8		vy	. . . . . . . . . 10 set y
9	8	cv 1618	. . . . . . . . 9 class y
10	9, 4	cfv 4659	. . . . . . . 8 class ( f ` y )
11	4, 9	cres 4649	. . . . . . . . 9 class ( f |` y )
12	11, 1	cfv 4659	. . . . . . . 8 class ( F ` ( f |` y ) )
13	10, 12	wceq 1619	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` y ) )
14	13, 8, 6	wral 2516	. . . . . 6 wff A. y e. x ( f ` y ) = ( F ` ( f |` y ) )
15	7, 14	wa 360	. . . . 5 wff ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) )
16		con0 4350	. . . . 5 class On
17	15, 5, 16	wrex 2517	. . . 4 wff E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) )
18	17, 3	cab 2242	. . 3 class { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
19	18	cuni 3787	. 2 class U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
20	2, 19	wceq 1619	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  6343  nfrecs  6344  recsfval  6351  tfrlem9  6355  dfrdg2  23507