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	$$⊢\phi \to FFnA$$
	wessf1orn.a	$$⊢\phi \to A\in V$$
	wessf1orn.r	$$⊢\phi \to R\mathrm{We}A$$
Assertion	wessf1orn	$$⊢\phi \to \exists x\in 𝒫A\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		wessf1orn.f	$$⊢\phi \to FFnA$$
2		wessf1orn.a	$$⊢\phi \to A\in V$$
3		wessf1orn.r	$$⊢\phi \to R\mathrm{We}A$$
4		eqid	$$⊢\left(y\in \mathrm{ran}F⟼\left(\iota x\in F^{-1}\left[\left\{y\right\}\right]|\forall z\in F^{-1}\left[\left\{y\right\}\right]\neg zRx\right)\right)=\left(y\in \mathrm{ran}F⟼\left(\iota x\in F^{-1}\left[\left\{y\right\}\right]|\forall z\in F^{-1}\left[\left\{y\right\}\right]\neg zRx\right)\right)$$
5	1 2 3 4	wessf1ornlem	$$⊢\phi \to \exists x\in 𝒫A\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}F$$