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

Definition df-recs 6592
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 6627 for more details on why this definition is desirable. Unlike df-rdg 6627 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 6620 and recsval 6621 for the primary contract of this definition.

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7457, zorn2 8342, and dfac8alem 7866. (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 6591 . 2  class recs ( F )
3 vf . . . . . . . 8  set  f
43cv 1648 . . . . . . 7  class  f
5 vx . . . . . . . 8  set  x
65cv 1648 . . . . . . 7  class  x
74, 6wfn 5408 . . . . . 6  wff  f  Fn  x
8 vy . . . . . . . . . 10  set  y
98cv 1648 . . . . . . . . 9  class  y
109, 4cfv 5413 . . . . . . . 8  class  ( f `
 y )
114, 9cres 4839 . . . . . . . . 9  class  ( f  |`  y )
1211, 1cfv 5413 . . . . . . . 8  class  ( F `
 ( f  |`  y ) )
1310, 12wceq 1649 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  y ) )
1413, 8, 6wral 2666 . . . . . 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 4541 . . . . 5  class  On
1715, 5, 16wrex 2667 . . . 4  wff  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) )
1817, 3cab 2390 . . 3  class  { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
1918cuni 3975 . 2  class  U. {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
202, 19wceq 1649 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  6593  nfrecs  6594  recsfval  6601  tfrlem9  6605  dfrdg2  25366
  Copyright terms: Public domain W3C validator