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

Library f_hartogs

initial import of the development

Require Export e_recursion.

Definition of Ordertypes and Proof that they are Ordinals


Definition ord M R x :=
  desc (fun a => ordiso (iseg M R x) a R).

Definition spec M R :=
  specification M (fun x => exists a, ordiso (iseg M R x) a R).

Definition ordertype M R :=
  replacement (spec M R) (fun x => ord M R x).

Lemma otype_empty R: ordertype empty R = empty.

Lemma otype_eliso M R a: a <e ordertype M R -> exists x, x <e M /\ ordiso (iseg M R x) a R.

Lemma otype_elord M R a: a <e ordertype M R -> ordinal a.

Lemma otype_stransitive M R: wordering R M -> stransitive (ordertype M R).

Theorem otype_ordinal M R: wordering R M -> ordinal (ordertype M R).

Proof that Ordertypes are Unique and Isomorphic to their Base-Set


Definition rep M R :=
  lam (ord M R) (spec M R).

Lemma spec_el M R x: x <e spec M R -> ordiso (iseg M R x) (ord M R x) R /\ x <e M.

Lemma ord_otype M R x: x <e spec M R -> ord M R x <e ordertype M R.

Lemma ord_ordinal M R x: x <e spec M R -> ordinal (ord M R x).

Lemma rep_el M R p: p <e rep M R -> (exists a, ordiso (iseg M R (pi1 p)) a R)
  -> ordinal (pi2 p).

Step 1: we prove that rep is an isomorphism between spec and ordertype.

Lemma ord_unique M R y x x': wordering R M -> x <e spec M R -> x' <e spec M R
  -> y = ord M R x -> y = ord M R x' -> x = x'.

Lemma rep_function M R: wordering R M -> function (rep M R) (spec M R) (ordertype M R).

Lemma rep_bijection M R: wordering R M -> bijection (rep M R) (spec M R) (ordertype M R).

Lemma ord_norder1 M R a b: wordering R M -> a <e spec M R -> b <e spec M R
  -> (a,b) <e R -> ord M R b = ord M R a -> False.

Lemma ord_norder2 M R a b: wordering R M -> a <e spec M R -> b <e spec M R
  -> (a,b) <e R -> ord M R b <e ord M R a -> False.

Lemma ord_order1 M R a b: wordering R M -> a <e spec M R -> b <e spec M R
  -> (a,b) <e R -> ord M R a <e ord M R b.

Lemma ord_order2 M R a b: wordering R M -> a <e spec M R -> b <e spec M R
  -> ord M R a <e ord M R b -> (a,b) <e R.

Lemma rep_opr M R: wordering R M -> opres (rep M R) (spec M R) R (elorder (ordertype M R)).

Theorem rep_oisomorphism M R: wordering R M
  -> oisomorphism (rep M R) (spec M R) (ordertype M R) R (elorder (ordertype M R)).

Corollary spec_ordiso M R: wordering R M -> ordiso (spec M R) (ordertype M R) R.

Step 2: now we prove that spec M = M for wellordered sets M.

Lemma spec_step x y M R: wordering R M -> x <e spec M R -> (y,x) <e R -> y <e spec M R.

Lemma spec_iseg_M M R: wordering R M -> spec M R = M \/
  exists x, x <e M /\ spec M R = iseg M R x.

Lemma spec_eq M R: wordering R M -> spec M R = M.

Step 3: the theorem follows by combining the results.

Theorem otype_ordiso M R: wordering R M -> ordiso M (ordertype M R) R.

Corollary otype_unique M R a: wordering R M -> ordiso M a R -> ordertype M R = a.

Theorem wo_ordiso M R: wordering R M -> (exists! a, ordiso M a R).

Corollary wo_ordinal M: WO M -> (exists a, ordinal a /\ equi M a).

Hartogs Numbers


Definition relations M :=
  product (power M) (power (product M M)).

Definition worder_space M :=
  specification (relations M) (fun p => wordering (pi2 p) (pi1 p)).

Definition h M :=
  replacement (worder_space M) (fun p => ordertype (pi1 p) (pi2 p)).

Lemma hartogs_el A: forall a, a <e (h A) -> ordinal a.

Theorem hartogs_ordinal A: ordinal (h A).

Lemma h_ordiso A: forall A', A' c= A -> ~ exists R, wordering R A' /\ ordiso A' (h A) R.

Theorem hartogs A: forall A', A' c= A -> ~ equi (h A) A'.