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

Definition df-recs 6592
 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-rdg 6627 for more details on why this definition is desirable. Unlike df-rdg 6627 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 6620 and recsval 6621 for the primary contract of this definition. EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7457, zorn2 8342, and dfac8alem 7866. (Contributed by Stefan O'Rear, 18-Jan-2015.) (New usage is discouraged.)
Assertion
Ref Expression
df-recs recs
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-recs
StepHypRef Expression
1 cF . . 3
21crecs 6591 . 2 recs
3 vf . . . . . . . 8
43cv 1648 . . . . . . 7
5 vx . . . . . . . 8
65cv 1648 . . . . . . 7
74, 6wfn 5408 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1648 . . . . . . . . 9
109, 4cfv 5413 . . . . . . . 8
114, 9cres 4839 . . . . . . . . 9
1211, 1cfv 5413 . . . . . . . 8
1310, 12wceq 1649 . . . . . . 7
1413, 8, 6wral 2666 . . . . . 6
157, 14wa 359 . . . . 5
16 con0 4541 . . . . 5
1715, 5, 16wrex 2667 . . . 4
1817, 3cab 2390 . . 3
1918cuni 3975 . 2
202, 19wceq 1649 1 recs
 Colors of variables: wff set class This definition is referenced by:  recseq  6593  nfrecs  6594  recsfval  6601  tfrlem9  6605  dfrdg2  25366
 Copyright terms: Public domain W3C validator