Definition df-recs 6385

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

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7244, zorn2 8130, and dfac8alem 7653. (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 6384	. 2 class recs ( F )
3		vf	. . . . . . . 8 set f
4	3	cv 1624	. . . . . . 7 class f
5		vx	. . . . . . . 8 set x
6	5	cv 1624	. . . . . . 7 class x
7	4, 6	wfn 5218	. . . . . 6 wff f Fn x
8		vy	. . . . . . . . . 10 set y
9	8	cv 1624	. . . . . . . . 9 class y
10	9, 4	cfv 5223	. . . . . . . 8 class ( f ` y )
11	4, 9	cres 4692	. . . . . . . . 9 class ( f |` y )
12	11, 1	cfv 5223	. . . . . . . 8 class ( F ` ( f |` y ) )
13	10, 12	wceq 1625	. . . . . . 7 wff ( f ` y ) = ( F ` ( f |` y ) )
14	13, 8, 6	wral 2546	. . . . . 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 4393	. . . . 5 class On
17	15, 5, 16	wrex 2547	. . . 4 wff E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) )
18	17, 3	cab 2272	. . 3 class { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
19	18	cuni 3830	. 2 class U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
20	2, 19	wceq 1625	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  6386  nfrecs  6387  recsfval  6394  tfrlem9  6398  dfrdg2  23555