Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-frecs Structured version   Visualization version   GIF version

Definition df-frecs 32729
Description: This is the definition for the founded recursion generator. Similar to df-wrecs 7805 and df-recs 7867, it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a founded set-like relationship for its properties, not a well-founded relationship. When this relationship is also a partial ordering, the proof does not use the Axiom of Infinity, but it requires Infinity when the order is not partial. We develop the theorems twice, once with partial ordering and once without. (Contributed by Scott Fenton, 23-Dec-2021.)
Assertion
Ref Expression
df-frecs frecs(𝑅, 𝐴, 𝐹) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Distinct variable groups:   𝑅,𝑓,𝑥,𝑦   𝐴,𝑓,𝑥,𝑦   𝑓,𝐹,𝑥,𝑦

Detailed syntax breakdown of Definition df-frecs
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
3 cF . . 3 class 𝐹
41, 2, 3cfrecs 32728 . 2 class frecs(𝑅, 𝐴, 𝐹)
5 vf . . . . . . . 8 setvar 𝑓
65cv 1524 . . . . . . 7 class 𝑓
7 vx . . . . . . . 8 setvar 𝑥
87cv 1524 . . . . . . 7 class 𝑥
96, 8wfn 6227 . . . . . 6 wff 𝑓 Fn 𝑥
108, 1wss 3865 . . . . . . 7 wff 𝑥𝐴
11 vy . . . . . . . . . . 11 setvar 𝑦
1211cv 1524 . . . . . . . . . 10 class 𝑦
131, 2, 12cpred 6029 . . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
1413, 8wss 3865 . . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1514, 11, 8wral 3107 . . . . . . 7 wff 𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1610, 15wa 396 . . . . . 6 wff (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
1712, 6cfv 6232 . . . . . . . 8 class (𝑓𝑦)
186, 13cres 5452 . . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
1912, 18, 3co 7023 . . . . . . . 8 class (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2017, 19wceq 1525 . . . . . . 7 wff (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2120, 11, 8wral 3107 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
229, 16, 21w3a 1080 . . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2322, 7wex 1765 . . . 4 wff 𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2423, 5cab 2777 . . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2524cuni 4751 . 2 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
264, 25wceq 1525 1 wff frecs(𝑅, 𝐴, 𝐹) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  frecseq123  32730  nffrecs  32731  frrlem5  32738
  Copyright terms: Public domain W3C validator