Metamath Proof Explorer


Theorem wfrrel

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

Proof

Step Hyp Ref Expression
1 wfrrel.1 F = wrecs R A G
2 df-wrecs wrecs R A G = frecs R A G 2 nd
3 1 2 eqtri F = frecs R A G 2 nd
4 3 frrrel Rel F