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

Definition df-recs 5898
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 5935 for more details on why this definition is desirable. Unlike df-irdg 5935 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 5927 and tfri2d 5928 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 5897 . 2  class recs ( F )
3 vf . . . . . . . 8  setvar  f
43cv 1242 . . . . . . 7  class  f
5 vx . . . . . . . 8  setvar  x
65cv 1242 . . . . . . 7  class  x
74, 6wfn 4875 . . . . . 6  wff  f  Fn  x
8 vy . . . . . . . . . 10  setvar  y
98cv 1242 . . . . . . . . 9  class  y
109, 4cfv 4880 . . . . . . . 8  class  ( f `
 y )
114, 9cres 4325 . . . . . . . . 9  class  ( f  |`  y )
1211, 1cfv 4880 . . . . . . . 8  class  ( F `
 ( f  |`  y ) )
1310, 12wceq 1243 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  y ) )
1413, 8, 6wral 2303 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) )
157, 14wa 97 . . . . 5  wff  ( f  Fn  x  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  y
) ) )
16 con0 4087 . . . . 5  class  On
1715, 5, 16wrex 2304 . . . 4  wff  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) )
1817, 3cab 2026 . . 3  class  { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
1918cuni 3577 . 2  class  U. {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
202, 19wceq 1243 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  5899  nfrecs  5900  recsfval  5909  tfrlem9  5913  tfr0  5915
  Copyright terms: Public domain W3C validator