I have some problems understanding the proof of the following theorem.
Given two well-ordered sets $(X, \le _X), \ (Y, \le _Y)$ there exists exactly one partial function $f(X, Y)$ such that:
1)$f: \ domf \rightarrow \ imf$ is a monotonic bijection
2) $domf, imf$ are such that $\forall x\in domf \ \ \forall y \in X : y <x \Rightarrow y \in domf$ and for $imf$ accordingly
3) $domf=X$ or $imf=Y$
When proving this, the function $f$ is defined in this way: $f$(min$X$)=min$Y$, $f(x^+)=(f(x))^+, \ f(x^+)=min(Y- \{ y : y \le x\}$ when x has no successor.
Then we take a family $F= \{f \subset X \times Y| \ f: X \rightarrow Y , \ 1), \ 2) \},$ ($(F, \subset) $ is a nonempty, partially ordered set)
and check that it satisfies Kuratowski-Zorn's Lemma and prove that a maximal element of $F$ also satisfies point 3).
Then we check uniqueness. We take $f_1, \ f_2$ and $X_0=domf_1$ as described in 2). Then $(X_0, \le _X)$ is well-ordered.
Consider $B:= \{ x\in X_0 | \ x \in domf_2, \ f_1(x)=f_2(x)\}$.
Then we check assumptions for transfinite induction, that is we assume that for $x_0 \in X \ \ (\leftarrow, x_0) \subset B$ and try to prove that then $x_0 \in B$.
I see that if $f_1$ is a monotonic injection, then $\forall x<x_0: f_1(x)<f_1(x_0) \ \Rightarrow f_1((\leftarrow, x)) \subset (\leftarrow, f_1(x_0))$. From what we assumed about $x_0$ we also know that $\forall x \in (\leftarrow, x_0): x\in domf_2$ and $f_1(x)=f_2(x)$, so $f_2((\leftarrow, x_0))=f_1((\leftarrow, x_0).$
And this is where I am lost: From 3): $domf_2 \neq (\leftarrow, x_0)\ \Rightarrow \exists z\in domf_2 : x_0 \le _X z$. Since $domf_1$ is as described in 3), then $x_0 \in domf_2 $.
Next, it is proven that $\forall j\in \{1,2 \}: f_j(x_0)=min (Y-f_j(\leftarrow, x_0)) $ and I know how to do that.
Do you think you could help me with that?
Thank a lot.
This should not require the Axiom of Choice (in the form of Zorn lemma). In fact, $F$ is totally ordered and we may simply take the union.
The one-line recursive definition $$ f(x)=\min\{y\in Y\mid \forall x'<x\colon f(x')<y\}$$ should work unless there occurs a $x$ for which $\{y\in Y\mid \forall x'<x\colon f(x')<y\}$ is empty, but then we already have a surjection.
For uniqueness, show that the sets $\operatorname{dom}(f_1)\setminus \operatorname{dom}(f_2)$, $\operatorname{dom}(f_2)\setminus \operatorname{dom}(f_1)$ and finally $\{x\in\operatorname{dom}(f_1)=\operatorname{dom}(f_2)\mid f_1(x)\ne f(x_2)\}$ are empty by obtaining a contradition from taking a minimal element.