Library g_proof
initial import of the development
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.
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.