Description: The well-ordered recursion generator generates a relation. Avoids the axiom of replacement. (Contributed by Scott Fenton, 8-Jun-2018) (Proof shortened by Scott Fenton, 17-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wfrrel.1 | |- F = wrecs ( R , A , G ) |
|
| Assertion | wfrrel | |- Rel F |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfrrel.1 | |- F = wrecs ( R , A , G ) |
|
| 2 | df-wrecs | |- wrecs ( R , A , G ) = frecs ( R , A , ( G o. 2nd ) ) |
|
| 3 | 1 2 | eqtri | |- F = frecs ( R , A , ( G o. 2nd ) ) |
| 4 | 3 | frrrel | |- Rel F |