Library c_ordinals

Require Export b_functions.

Definition succ a := bunion a (singleton a).
Definition zero := empty.
Definition one := succ zero.

Definition stransitive A := forall x, x <e A -> x c= A.
Definition elorder A := specification (product A A) (fun p => pi1 p <e pi2 p).
Definition ordinal a := stransitive a /\ wordering (elorder a) a.

Lemma empty_ordinal: ordinal empty.

Lemma elorder_el a b A: a <e b -> a <e A -> b <e A -> (a,b) <e elorder A.

Lemma elorder_el' a b A: (a,b) <e elorder A -> a <e A /\ b <e A /\ a <e b.

Lemma elorder_element A a b: (a,b) <e elorder A -> a <e b.

Lemma elorder_res a b: a c= b -> (elorder b)|> a = elorder a.

Lemma succ_subs A B: A c= B -> A c= succ B.

Lemma succ_el A: A <e succ A.

Lemma succ_subset A: A c= succ A.

Lemma el_succ b a: ordinal a -> b <e a -> succ b c= succ a.

Lemma el_succ_subs b a: ordinal a -> b <e a -> succ b c= a.

Lemma succ_fun f A B: function f A (succ B) -> B /<e ran f -> function f A B.

Lemma succ_trans A x: x <e A -> x <e succ A.

Lemma elorder_subs A A' a b: A' c= A -> (a,b) <e elorder A' -> (a,b) <e elorder A.

Lemma elorder_succ A a b: (a,b) <e elorder A -> (a,b) <e elorder (succ A).

Lemma el_su A A' a b: (a,b) <e elorder A -> a <e A' -> b <e A' -> (a,b) <e elorder A'.

Lemma elorder_trans a x y z: transitive (elorder a) -> x <e a -> y <e a -> z <e a ->
  x <e y -> y <e z -> x <e z.

Lemma elorder_worder M M': M' c= M -> wordering (elorder M) M -> wordering (elorder M') M'.

Lemma ordinal_el a a': ordinal a -> a' <e a -> ordinal a'.

Lemma ordinal_eltrans a x: ordinal a -> x <e a -> stransitive x.

Lemma ordinal_subs x y: ordinal x -> ordinal y -> x <> y -> x c= y -> x <e y.

Lemma ordinal_nel a: ordinal a -> a /<e a.

Lemma ordinal_trans x y z: ordinal x -> ordinal y -> ordinal z -> x <e y -> y <e z -> x <e z.

Lemma ordinal_anti x y: ordinal x -> ordinal y -> x <e y -> y /<e x.

Lemma ordinal_inter x y: ordinal x -> ordinal y -> ordinal (binter x y).

Lemma ordinal_linear x y: ordinal x -> ordinal y -> x <e y \/ x = y \/ y <e x.

Lemma elorder_linear M: (forall a, a <e M -> ordinal a) -> linear (elorder M) M.

Lemma ordinal_wfounded M: (forall a, a <e M -> ordinal a) -> M <> empty ->
  exists a, a <e M /\ forall b, b <e M -> a <e b \/ a = b.

Lemma ordinal_set_asym M: (forall a, a <e M -> ordinal a) -> asymmetric (elorder M).

Lemma ordinal_set_trans M: (forall a, a <e M -> ordinal a) -> transitive (elorder M).

Lemma ordinal_set_wf M: (forall a, a <e M -> ordinal a) -> wfounded (elorder M) M.

Theorem ordinal_set M: (forall a, a <e M -> ordinal a) -> wordering (elorder M) M.

Corollary succ_ordinal a: ordinal a -> ordinal (succ a).

Corollary ordinal_union M: (forall a, a <e M -> ordinal a) -> ordinal (union M).

Corollary ordinal_bunion a b: ordinal a -> ordinal b -> ordinal (bunion a b).

Corollary ordinal_noset: ~ exists O, forall a, (ordinal a -> a <e O) /\ (a <e O -> ordinal a).

Corollary ordinals_sosubset: ~ exists O, forall a, ordinal a -> a <e O.

Definition iorder M a f :=
  specification (product M M) (fun p => (f[pi1 p],f[pi2 p]) <e elorder a).

Lemma iorder_el M a f x y: (x,y) <e (iorder M a f) -> (f[x], f[y]) <e elorder a.

Lemma iorder_el' M a f x y: (f[x], f[y]) <e elorder a
  -> x <e M -> y <e M -> (x,y) <e (iorder M a f).

Lemma iorder_dom1 M a f x y: (x,y) <e (iorder M a f) -> x <e M.

Lemma iorder_dom2 M a f x y: (x,y) <e (iorder M a f) -> y <e M.

Lemma iorder_asym M a f: ordinal a -> asymmetric (iorder M a f).

Lemma iorder_trans M a f: ordinal a -> transitive (iorder M a f).

Lemma iorder_lin M a f: ordinal a -> bijection f M a -> linear (iorder M a f) M.

Lemma iorder_wf M a f: ordinal a -> bijection f M a -> wfounded (iorder M a f) M.

Theorem ordinal_iorder M a f: ordinal a -> bijection f M a -> wordering (iorder M a f) M.

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