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 32107
Description: This is the definition for the founded recursion generator. Similar to df-wrecs 7558 and df-recs 7620, 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. However, the proof of this requires the Axiom of Infinity, so we retain the other definitions since their properties do not require it. (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 32106 . 2 class frecs(𝑅, 𝐴, 𝐹)
5 vf . . . . . . . 8 setvar 𝑓
65cv 1629 . . . . . . 7 class 𝑓
7 vx . . . . . . . 8 setvar 𝑥
87cv 1629 . . . . . . 7 class 𝑥
96, 8wfn 6026 . . . . . 6 wff 𝑓 Fn 𝑥
108, 1wss 3721 . . . . . . 7 wff 𝑥𝐴
11 vy . . . . . . . . . . 11 setvar 𝑦
1211cv 1629 . . . . . . . . . 10 class 𝑦
131, 2, 12cpred 5822 . . . . . . . . 9 class Pred(𝑅, 𝐴, 𝑦)
1413, 8wss 3721 . . . . . . . 8 wff Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1514, 11, 8wral 3060 . . . . . . 7 wff 𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥
1610, 15wa 382 . . . . . 6 wff (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)
1712, 6cfv 6031 . . . . . . . 8 class (𝑓𝑦)
186, 13cres 5251 . . . . . . . . 9 class (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))
1912, 18, 3co 6792 . . . . . . . 8 class (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2017, 19wceq 1630 . . . . . . 7 wff (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
2120, 11, 8wral 3060 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
229, 16, 21w3a 1070 . . . . 5 wff (𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2322, 7wex 1851 . . . 4 wff 𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
2423, 5cab 2756 . . 3 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2524cuni 4572 . 2 class {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
264, 25wceq 1630 1 wff frecs(𝑅, 𝐴, 𝐹) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  frecseq123  32108  nffrecs  32109  frrlem6  32120  frrlem7  32121  frrlem10  32122  frrlem11  32123
  Copyright terms: Public domain W3C validator