Library f_hartogs
initial import of the development
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).
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).
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'.