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

Definition df-recs 5861
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 5897 for more details on why this definition is desirable. Unlike df-irdg 5897 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 5890 and tfri2d 5891 for the primary contract of this definition.

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

Assertion
Ref Expression
df-recs recs F  U. {  |  On  Fn  `  F `  |`  }
Distinct variable group:   , F,,

Detailed syntax breakdown of Definition df-recs
StepHypRef Expression
1 cF . . 3  F
21crecs 5860 . 2 recs F
3 vf . . . . . . . 8  setvar
43cv 1241 . . . . . . 7
5 vx . . . . . . . 8  setvar
65cv 1241 . . . . . . 7
74, 6wfn 4840 . . . . . 6  Fn
8 vy . . . . . . . . . 10  setvar
98cv 1241 . . . . . . . . 9
109, 4cfv 4845 . . . . . . . 8  `
114, 9cres 4290 . . . . . . . . 9  |`
1211, 1cfv 4845 . . . . . . . 8  F `
 |`
1310, 12wceq 1242 . . . . . . 7  `  F `  |`
1413, 8, 6wral 2300 . . . . . 6  `  F `  |`
157, 14wa 97 . . . . 5  Fn  `  F `  |`
16 con0 4066 . . . . 5  On
1715, 5, 16wrex 2301 . . . 4  On  Fn  `  F `  |`
1817, 3cab 2023 . . 3  {  |  On  Fn  `  F `  |`  }
1918cuni 3571 . 2  U. {  |  On  Fn  `  F `  |`  }
202, 19wceq 1242 1 recs F  U. {  |  On  Fn  `  F `  |`  }
Colors of variables: wff set class
This definition is referenced by:  recseq  5862  nfrecs  5863  recsfval  5872  tfrlem9  5876  tfr0  5878
  Copyright terms: Public domain W3C validator