Metamath Proof Explorer


Theorem wessf1orn

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 φFFnA
wessf1orn.a φAV
wessf1orn.r φRWeA
Assertion wessf1orn φx𝒫AFx:x1-1 ontoranF

Proof

Step Hyp Ref Expression
1 wessf1orn.f φFFnA
2 wessf1orn.a φAV
3 wessf1orn.r φRWeA
4 eqid yranFιxF-1y|zF-1y¬zRx=yranFιxF-1y|zF-1y¬zRx
5 1 2 3 4 wessf1ornlem φx𝒫AFx:x1-1 ontoranF