Metamath Proof Explorer


Theorem wfrfun

Description: The "function" generated by the well-ordered recursion generator is indeed a function. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by Scott Fenton, 17-Nov-2024)

Ref Expression
Hypothesis wfrfun.1 F=wrecsRAG
Assertion wfrfun RWeARSeAFunF

Proof

Step Hyp Ref Expression
1 wfrfun.1 F=wrecsRAG
2 wefr RWeARFrA
3 2 adantr RWeARSeARFrA
4 weso RWeAROrA
5 sopo ROrARPoA
6 4 5 syl RWeARPoA
7 6 adantr RWeARSeARPoA
8 simpr RWeARSeARSeA
9 df-wrecs wrecsRAG=frecsRAG2nd
10 1 9 eqtri F=frecsRAG2nd
11 10 fprfung RFrARPoARSeAFunF
12 3 7 8 11 syl3anc RWeARSeAFunF