Browse the main library: A B C D E F G or go to appendix or return to overview.

# Library g_proof

initial import of the development

Require Export f_hartogs.

We define the refactored powerset pow' that does not contain the empty set. Next, we formulate the definition of the Axiom of Choice.

Definition pow' M :=
(power M)\singleton empty.

Definition AC M :=
exists c, function c (pow' M) M /\ forall M', M' <> empty -> M' c= M -> c[M'] <e M'.

Lemma pow_subs M M': M' <e pow' M -> M' c= M.

Lemma pow_nempty M M': M' <e pow' M -> M' <> empty.

## The Well-Ordering Theorem

Section proof.
Variable M: set.
Variable c: set.
Variable choice: forall M', M' <> empty -> M' c= M -> c[M'] <e M'.

Definition doms := succ (h M).
Definition sequences := space doms (succ M).
Definition bran f := specification M (fun x => x <e ran f).

We define g as the function, that takes a transfinite sequence of elements of M, tests whether there are some elements left and return either the choice on the rest, or the dummy element M, respecitively. Transfinite Recursion returns a sequence f, that contains all these successive choices.

Definition g := specification (product sequences (succ M))
(fun p => M\(ran (pi1 p)) <> empty /\ c[M\(ran (pi1 p)) ] = pi2 p
\/ M\(ran (pi1 p)) = empty /\ M = pi2 p).

Definition f :=
desc (fun f => function f doms (succ M) /\ forall a', a' <e doms -> f[a'] = g[f|a']).

Definition R := specification doms (fun a' => f[a'] = M).
Definition a := desc (fun a => least (elorder doms) R a).

Lemma doms_ordinal: ordinal doms.

Lemma doms_str: stransitive doms.

Lemma fg: function g sequences (succ M).

Lemma rec: function f doms (succ M) /\ forall a', a' <e doms -> f[a'] = g[f|a'].

Lemma ff: function f doms (succ M).

Lemma g2f: forall a' : set, a' <e doms -> f [a'] = g [f | a'].

Lemma f_rel: relation f doms (succ M).

Lemma R_subs: R c= doms.

Lemma f_seq: forall a, a <e doms -> f|a <e sequences.

Lemma exhausted: forall a, a <e doms -> f[a] = M -> M c= ran (f|a).

Lemma ran_subs: forall a b, a <e b -> ordinal b -> ran f|a c= ran f|b.

We prove two important results: f is injective unless all elements of M were collected, and the set R of all ordinals that exhaust M is not empty. This will yield a minimum a, such that f restricted to this minimum is a bijection of M and a.

Lemma f_inj: forall a, (forall x, x <e a -> M\(ran (f|x)) <> empty) -> injective f|a.

Lemma R_ne: R <> empty.

Lemma a_least: least (elorder doms) R a.

Lemma a_R: a <e R.

Lemma a_el: a <e doms.

Lemma a_subs: a c= doms.

Lemma a_ordinal: ordinal a.

Lemma a_inf: forall b, b <e R -> (a,b) <e (elorder doms) \/ b = a.

Lemma a_ex: forall l, l <e a -> M\(ran (f|l)) <> empty.

Lemma fa_M: M /<e ran f|a.

Lemma fa_fun: function f|a a M.

Lemma fa_ran: ran f|a = M.

Lemma fa_surjective: surjective f|a a M.

Lemma Z: WO M.
End proof.

## Equivalence

Theorem Zermelo M: AC M -> WO M.

Theorem Olemrez M: WO M -> AC M.