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

Definition df-recs 7061
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 7095 for more details on why this definition is desirable. Unlike df-rdg 7095 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 7088 and recsval 7089 for the primary contract of this definition.

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7978, zorn2 8907, and dfac8alem 8431. (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 7060 . 2
3 vf . . . . . . . 8
43cv 1394 . . . . . . 7
5 vx . . . . . . . 8
65cv 1394 . . . . . . 7
74, 6wfn 5588 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1394 . . . . . . . . 9
109, 4cfv 5593 . . . . . . . 8
114, 9cres 5006 . . . . . . . . 9
1211, 1cfv 5593 . . . . . . . 8
1310, 12wceq 1395 . . . . . . 7
1413, 8, 6wral 2807 . . . . . 6
157, 14wa 369 . . . . 5
16 con0 4883 . . . . 5
1715, 5, 16wrex 2808 . . . 4
1817, 3cab 2442 . . 3
1918cuni 4249 . 2
202, 19wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  recseq  7062  nfrecs  7063  recsfval  7069  tfrlem9  7073  dfrdg2  29228
  Copyright terms: Public domain W3C validator