Description: Given a function F on a well-ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wessf1orn.f | |
|
wessf1orn.a | |
||
wessf1orn.r | |
||
Assertion | wessf1orn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wessf1orn.f | |
|
2 | wessf1orn.a | |
|
3 | wessf1orn.r | |
|
4 | eqid | |
|
5 | 1 2 3 4 | wessf1ornlem | |