This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → F Fn A
wessf1orn.a ⊢ φ → A ∈ V
wessf1orn.r ⊢ φ → R We A
Assertion wessf1orn ⊢ φ → ∃ x ∈ 𝒫 A F ↾ x : x ⟶ 1-1 onto ran ⁡ F

Proof

Step Hyp Ref Expression
1 wessf1orn.f ⊢ φ → F Fn A
2 wessf1orn.a ⊢ φ → A ∈ V
3 wessf1orn.r ⊢ φ → R We A
4 eqid ⊢ y ∈ ran ⁡ F ⟼ ι x ∈ F -1 y | ∀ z ∈ F -1 y ¬ z R x = y ∈ ran ⁡ F ⟼ ι x ∈ F -1 y | ∀ z ∈ F -1 y ¬ z R x
5 1 2 3 4 wessf1ornlem ⊢ φ → ∃ x ∈ 𝒫 A F ↾ x : x ⟶ 1-1 onto ran ⁡ F