Definition df-recs 6662

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

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7530, zorn2 8417, and dfac8alem 7941. (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 6661	. 2 class recs ( F )
3		vf	. . . . . . . 8 set f
4	3	cv 1652	. . . . . . 7 class f
5		vx	. . . . . . . 8 set x
6	5	cv 1652	. . . . . . 7 class x
7	4, 6	wfn 5478	. . . . . 6 wff f Fn x
8		vy	. . . . . . . . . 10 set y
9	8	cv 1652	. . . . . . . . 9 class y
10	9, 4	cfv 5483	. . . . . . . 8 class ( f ` y )
11	4, 9	cres 4909	. . . . . . . . 9 class ( f |` y )
12	11, 1	cfv 5483	. . . . . . . 8 class ( F ` ( f |` y ) )
13	10, 12	wceq 1653	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` y ) )
14	13, 8, 6	wral 2711	. . . . . 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 4610	. . . . 5 class On
17	15, 5, 16	wrex 2712	. . . 4 wff E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) )
18	17, 3	cab 2428	. . 3 class { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
19	18	cuni 4039	. 2 class U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
20	2, 19	wceq 1653	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  6663  nfrecs  6664  recsfval  6671  tfrlem9  6675  dfrdg2  25454