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

Definition df-recs 6791
Description: Define a function on , the class of ordinal numbers, by transfinite recursion given a rule which sets the next value given all values so far. See df-rdg 6825 for more details on why this definition is desirable. Unlike df-rdg 6825 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 6818 and recsval 6819 for the primary contract of this definition.

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7693, zorn2 8622, and dfac8alem 8146. (Contributed by Stefan O'Rear, 18-Jan-2015.) (New usage is discouraged.)

Assertion
Ref Expression
df-recs
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-recs
StepHypRef Expression
1 cF . . 3
21crecs 6790 . 2
3 vf . . . . . . . 8
43cv 1686 . . . . . . 7
5 vx . . . . . . . 8
65cv 1686 . . . . . . 7
74, 6wfn 5385 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1686 . . . . . . . . 9
109, 4cfv 5390 . . . . . . . 8
114, 9cres 4813 . . . . . . . . 9
1211, 1cfv 5390 . . . . . . . 8
1310, 12wceq 1687 . . . . . . 7
1413, 8, 6wral 2694 . . . . . 6
157, 14wa 362 . . . . 5
16 con0 4690 . . . . 5
1715, 5, 16wrex 2695 . . . 4
1817, 3cab 2408 . . 3
1918cuni 4066 . 2
202, 19wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  recseq  6792  nfrecs  6793  recsfval  6799  tfrlem9  6803  dfrdg2  27311
  Copyright terms: Public domain W3C validator