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 | |
|
Assertion | wfrfun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wfrfun.1 | |
|
2 | wefr | |
|
3 | 2 | adantr | |
4 | weso | |
|
5 | sopo | |
|
6 | 4 5 | syl | |
7 | 6 | adantr | |
8 | simpr | |
|
9 | df-wrecs | |
|
10 | 1 9 | eqtri | |
11 | 10 | fprfung | |
12 | 3 7 8 11 | syl3anc | |