This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-frecs

Description: This is the definition for the well-founded recursion generator. Similar to df-wrecs and df-recs , it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a well-founded set-like relationship for its properties, not a well-ordered relationship. This proof requires either a partial order or the axiom of infinity. We develop the theorems twice, once with a partial order and once without. The second development occurs later in the database, after ax-inf has been introduced. (Contributed by Scott Fenton, 23-Dec-2021)

Ref Expression
Assertion df-frecs ⊢ frecs ⁡ R A F = ⋃ f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y F f ↾ Pred R A y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 cA class A
2 cF class F
3 1 0 2 cfrecs class frecs ⁡ R A F
4 vf setvar f
5 vx setvar x
6 4 cv setvar f
7 5 cv setvar x
8 6 7 wfn wff f Fn x
9 7 1 wss wff x ⊆ A
10 vy setvar y
11 10 cv setvar y
12 1 0 11 cpred class Pred R A y
13 12 7 wss wff Pred R A y ⊆ x
14 13 10 7 wral wff ∀ y ∈ x Pred R A y ⊆ x
15 9 14 wa wff x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x
16 11 6 cfv class f ⁡ y
17 6 12 cres class f ↾ Pred R A y
18 11 17 2 co class y F f ↾ Pred R A y
19 16 18 wceq wff f ⁡ y = y F f ↾ Pred R A y
20 19 10 7 wral wff ∀ y ∈ x f ⁡ y = y F f ↾ Pred R A y
21 8 15 20 w3a wff f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y F f ↾ Pred R A y
22 21 5 wex wff ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y F f ↾ Pred R A y
23 22 4 cab class f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y F f ↾ Pred R A y
24 23 cuni class ⋃ f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y F f ↾ Pred R A y
25 3 24 wceq wff frecs ⁡ R A F = ⋃ f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y F f ↾ Pred R A y