MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-recs Structured version   Unicode version

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
StepHypRef Expression
1 cF . . 3  class  F
21crecs 6661 . 2  class recs ( F )
3 vf . . . . . . . 8  set  f
43cv 1652 . . . . . . 7  class  f
5 vx . . . . . . . 8  set  x
65cv 1652 . . . . . . 7  class  x
74, 6wfn 5478 . . . . . 6  wff  f  Fn  x
8 vy . . . . . . . . . 10  set  y
98cv 1652 . . . . . . . . 9  class  y
109, 4cfv 5483 . . . . . . . 8  class  ( f `
 y )
114, 9cres 4909 . . . . . . . . 9  class  ( f  |`  y )
1211, 1cfv 5483 . . . . . . . 8  class  ( F `
 ( f  |`  y ) )
1310, 12wceq 1653 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  y ) )
1413, 8, 6wral 2711 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) )
157, 14wa 360 . . . . 5  wff  ( f  Fn  x  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  y
) ) )
16 con0 4610 . . . . 5  class  On
1715, 5, 16wrex 2712 . . . 4  wff  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) )
1817, 3cab 2428 . . 3  class  { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
1918cuni 4039 . 2  class  U. {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
202, 19wceq 1653 1  wff recs ( F )  =  U. {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  recseq  6663  nfrecs  6664  recsfval  6671  tfrlem9  6675  dfrdg2  25454
  Copyright terms: Public domain W3C validator