Definition df-recs 6625

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

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7493, zorn2 8378, and dfac8alem 7902. (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 6624	. 2 class recs ( F )
3		vf	. . . . . . . 8 set f
4	3	cv 1651	. . . . . . 7 class f
5		vx	. . . . . . . 8 set x
6	5	cv 1651	. . . . . . 7 class x
7	4, 6	wfn 5441	. . . . . 6 wff f Fn x
8		vy	. . . . . . . . . 10 set y
9	8	cv 1651	. . . . . . . . 9 class y
10	9, 4	cfv 5446	. . . . . . . 8 class ( f ` y )
11	4, 9	cres 4872	. . . . . . . . 9 class ( f |` y )
12	11, 1	cfv 5446	. . . . . . . 8 class ( F ` ( f |` y ) )
13	10, 12	wceq 1652	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` y ) )
14	13, 8, 6	wral 2697	. . . . . 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 4573	. . . . 5 class On
17	15, 5, 16	wrex 2698	. . . 4 wff E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) )
18	17, 3	cab 2421	. . 3 class { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
19	18	cuni 4007	. 2 class U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
20	2, 19	wceq 1652	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  6626  nfrecs  6627  recsfval  6634  tfrlem9  6638  dfrdg2  25415