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

Definition df-recs 6388
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 6423 for more details on why this definition is desirable. Unlike df-rdg 6423 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 6416 and recsval 6417 for the primary contract of this definition.

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7247, zorn2 8133, and dfac8alem 7656. (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 6387 . 2  class recs ( F )
3 vf . . . . . . . 8  set  f
43cv 1622 . . . . . . 7  class  f
5 vx . . . . . . . 8  set  x
65cv 1622 . . . . . . 7  class  x
74, 6wfn 5250 . . . . . 6  wff  f  Fn  x
8 vy . . . . . . . . . 10  set  y
98cv 1622 . . . . . . . . 9  class  y
109, 4cfv 5255 . . . . . . . 8  class  ( f `
 y )
114, 9cres 4691 . . . . . . . . 9  class  ( f  |`  y )
1211, 1cfv 5255 . . . . . . . 8  class  ( F `
 ( f  |`  y ) )
1310, 12wceq 1623 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  y ) )
1413, 8, 6wral 2543 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) )
157, 14wa 358 . . . . 5  wff  ( f  Fn  x  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  y
) ) )
16 con0 4392 . . . . 5  class  On
1715, 5, 16wrex 2544 . . . 4  wff  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) )
1817, 3cab 2269 . . 3  class  { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
1918cuni 3827 . 2  class  U. {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
202, 19wceq 1623 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  6389  nfrecs  6390  recsfval  6397  tfrlem9  6401  dfrdg2  24152
  Copyright terms: Public domain W3C validator