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

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
StepHypRef Expression
1 cF . . 3  class  F
21crecs 6624 . 2  class recs ( F )
3 vf . . . . . . . 8  set  f
43cv 1651 . . . . . . 7  class  f
5 vx . . . . . . . 8  set  x
65cv 1651 . . . . . . 7  class  x
74, 6wfn 5441 . . . . . 6  wff  f  Fn  x
8 vy . . . . . . . . . 10  set  y
98cv 1651 . . . . . . . . 9  class  y
109, 4cfv 5446 . . . . . . . 8  class  ( f `
 y )
114, 9cres 4872 . . . . . . . . 9  class  ( f  |`  y )
1211, 1cfv 5446 . . . . . . . 8  class  ( F `
 ( f  |`  y ) )
1310, 12wceq 1652 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  y ) )
1413, 8, 6wral 2697 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) )
157, 14wa 359 . . . . 5  wff  ( f  Fn  x  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  y
) ) )
16 con0 4573 . . . . 5  class  On
1715, 5, 16wrex 2698 . . . 4  wff  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) )
1817, 3cab 2421 . . 3  class  { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
1918cuni 4007 . 2  class  U. {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
202, 19wceq 1652 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  6626  nfrecs  6627  recsfval  6634  tfrlem9  6638  dfrdg2  25415
  Copyright terms: Public domain W3C validator