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

Definition df-recs 5920
 Description: Define a function recs on , the class of ordinal numbers, by transfinite recursion given a rule which sets the next value given all values so far. See df-irdg 5957 for more details on why this definition is desirable. Unlike df-irdg 5957 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 5949 and tfri2d 5950 for the primary contract of this definition. (Contributed by Stefan O'Rear, 18-Jan-2015.)
Assertion
Ref Expression
df-recs recs
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-recs
StepHypRef Expression
1 cF . . 3
21crecs 5919 . 2 recs
3 vf . . . . . . . 8
43cv 1242 . . . . . . 7
5 vx . . . . . . . 8
65cv 1242 . . . . . . 7
74, 6wfn 4897 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1242 . . . . . . . . 9
109, 4cfv 4902 . . . . . . . 8
114, 9cres 4347 . . . . . . . . 9
1211, 1cfv 4902 . . . . . . . 8
1310, 12wceq 1243 . . . . . . 7
1413, 8, 6wral 2306 . . . . . 6
157, 14wa 97 . . . . 5
16 con0 4100 . . . . 5
1715, 5, 16wrex 2307 . . . 4
1817, 3cab 2026 . . 3
1918cuni 3580 . 2
202, 19wceq 1243 1 recs
 Colors of variables: wff set class This definition is referenced by:  recseq  5921  nfrecs  5922  recsfval  5931  tfrlem9  5935  tfr0  5937
 Copyright terms: Public domain W3C validator