## An alternative to Zorn's lemma

This page is a draft. The bulk of it was moved to 4.6

The following theorem is independent of the axiom of choice, but the results in set theory traditionally deduced from Zorn's lemma can instead be deduced from this together with an elementary expression of the axiom of choice.

Theorem. Let φ a function whose domain D is a set of sets, such thatxD, φ(x)∉x. Then there exists a unique subset KD satisfying the following properties

• The restriction φ|K is injective
• ∀x∈K, x⊂φ[K]
• The binary relation on K defined by (x,y)↦(φ(x)∈y)  is a strict well-ordering
• φ[K]∉D.

Proof.

Note : I'm not satisfied with this proof that is quite long and complicated. I hope to find a more elegant proof (through more interesting intermediate steps) in the future. In particular I'll surely re-write it as a consequence of Tarski's Fixed Point Theorem.

Let f be the function from P(D) to itself defined by:

• xD, f({x}) =  {x∪{φ(x)}} if x∪{φ(x)}∈ D, or ∅ otherwise
• For any other A⊂D, f(A) = {∪A} if ∪A ∈ D, or ∅ otherwise. In particular, f(∅) = {∅}
Then let K be the smallest subset of D stable by f (such that ∀AK, f(A)⊂K). By the fixed point theorem, ∀xD, xK⇔(x=∅∨(∃yK, x = y∪{φ(y)})∨(∃A ⊂ K, x = ∪A)).

xK,∀Ax, (∀y,y'K, (yA ∧ (y∪{φ(y)}= y'⊂x))⇒y'⊂A))⇒A=x because
If (∀y,y'∈K, ((yA)∧ y∪{φ(y)}= y'⊂x)⇒y'⊂A)), then the set C={z∈K| z⊂x⇒z⊂A}is stable by f. Thus C=K. But x∈K, thus x⊂x⇒x⊂A. Finally A=x.
x,yK, (x⊂y ∨ yx) because
Let us show that C={xK|∀yK, xyyx}is stable by f. The stability by unions is straightforward :
AC, ∀yK, ((∃xA, yx)⇒y⊂∪A ) and ((∀x∈A, xy)⇒∪Ay)
Then ∀xC, ∀x',zK, x' = x∪{φ(x)}⇒((zxx')∨(xz)). Now if xz and φ(x)∉z then (∀y,y'∈K, (y⊂x ∧ y∪{φ(y)}= y'⊂z)⇒(x=y'∨x⊄y')⇒y'⊂x), so that x=z according to the above, and z⊂x'. In the other case of x⊂z and φ(x)∈z we have x'⊂z. Finally x'∈C.
Thus C is stable by f, thus C=K, thus ∀x,yK, (x⊂y ∨ y⊂x).
x,yK ,  (x⊂y ∧ x∪{φ(x)}∉K) ⇒x=y because
∀z,z'K, (zx ∧ (z∪{φ(z)}= z'⊂y))⇒ (z'=x ∨ x⊄z') ⇒ z'⊂x.
The restriction φ|K is injective because
xyK, φ(x)=φ(y)⇒φ(x)∉y ⇒(x∪{φ(x)}∉Ky = x)⇒x=y.

(To be continued).