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	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	wessf1orn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	wessf1orn.r	⊢ ( 𝜑 → 𝑅 We 𝐴 )
Assertion	wessf1orn	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		wessf1orn.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		wessf1orn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		wessf1orn.r	⊢ ( 𝜑 → 𝑅 We 𝐴 )
4		eqid	⊢ ( 𝑦 ∈ ran 𝐹 ↦ ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ¬ 𝑧 𝑅 𝑥 ) ) = ( 𝑦 ∈ ran 𝐹 ↦ ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ¬ 𝑧 𝑅 𝑥 ) )
5	1 2 3 4	wessf1ornlem	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐹 )