ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-recs Unicode version

Definition df-recs 5950
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-irdg 5987 for more details on why this definition is desirable. Unlike df-irdg 5987 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 tfri1d 5979 and tfri2d 5980 for the primary contract of this definition.

(Contributed by Stefan O'Rear, 18-Jan-2015.)

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 5949 . 2  class recs ( F )
3 vf . . . . . . . 8  setvar  f
43cv 1258 . . . . . . 7  class  f
5 vx . . . . . . . 8  setvar  x
65cv 1258 . . . . . . 7  class  x
74, 6wfn 4924 . . . . . 6  wff  f  Fn  x
8 vy . . . . . . . . . 10  setvar  y
98cv 1258 . . . . . . . . 9  class  y
109, 4cfv 4929 . . . . . . . 8  class  ( f `
 y )
114, 9cres 4374 . . . . . . . . 9  class  ( f  |`  y )
1211, 1cfv 4929 . . . . . . . 8  class  ( F `
 ( f  |`  y ) )
1310, 12wceq 1259 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  y ) )
1413, 8, 6wral 2323 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) )
157, 14wa 101 . . . . 5  wff  ( f  Fn  x  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  y
) ) )
16 con0 4127 . . . . 5  class  On
1715, 5, 16wrex 2324 . . . 4  wff  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) )
1817, 3cab 2042 . . 3  class  { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
1918cuni 3607 . 2  class  U. {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
202, 19wceq 1259 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  5951  nfrecs  5952  recsfval  5961  tfrlem9  5965  tfr0  5967
  Copyright terms: Public domain W3C validator