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.


Theorem Zermelo M: AC M -> WO M.

Theorem Olemrez M: WO M -> AC M.