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	|- ( ph -> F Fn A )
	wessf1orn.a	|- ( ph -> A e. V )
	wessf1orn.r	|- ( ph -> R We A )
Assertion	wessf1orn	|- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )

Proof

Step	Hyp	Ref	Expression
1		wessf1orn.f	|- ( ph -> F Fn A )
2		wessf1orn.a	|- ( ph -> A e. V )
3		wessf1orn.r	|- ( ph -> R We A )
4		eqid	|- ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) ) = ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) )
5	1 2 3 4	wessf1ornlem	|- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )