Library d_isomorphy

Require Export c_ordinals.

Definition iseg M R x :=
  specification M (fun y => (y,x) <e R).

Definition oiseg a x :=
  specification a (fun y => y <e x).

Lemma iseg_nel x M R: wordering R M -> x /<e iseg M R x.

Lemma iseg_el M R x y: x <e iseg M R y -> (x,y) <e R.

Lemma iseg_subs x y M R: wordering R M -> (x,y) <e R -> iseg M R x c= iseg M R y.

Lemma iseg_eq M R y x: wordering R M -> (y,x) <e R -> iseg (iseg M R x) R y = iseg M R y.

Lemma oiseg_eq a b: a c= b -> a = oiseg b a.

Lemma oiseg_lin a b: ordinal a -> ordinal b -> a = oiseg b a \/ b = oiseg a b.

Lemma iseg_worder M R x x': wordering R M -> x <e M -> x' <e M
  -> (iseg M R x) = (iseg M R x') -> (x,x') /<e R.

Lemma iseg_equal M R x x': wordering R M -> x <e M -> x' <e M
  -> (iseg M R x) = (iseg M R x') -> x = x'.

Lemma iseg_ordinal_eq a b: ordinal a -> b <e a -> iseg a (elorder a) b = b.

Lemma iseg_ordinal a b: ordinal a -> b <e a -> ordinal (iseg a (elorder a) b).

Lemma iseg_res A R x: x <e A -> iseg A (R|>A) x = iseg A R x.

Definition opres f A R S :=
  (forall a b, a <e A -> b <e A -> ((a,b) <e R <-> (f[a],f[b]) <e S)).

Definition oisomorphism f A B R S :=
  bijection f A B /\ opres f A R S.

Definition oiso A B R S :=
  exists f, oisomorphism f A B R S.

Definition ordiso M a R :=
  ordinal a /\ oiso M a R (elorder a).

Lemma oiso_ref A R: oiso A A R R.

Lemma oiso_com A B R S: oiso A B R S -> oiso B A S R.

Lemma oiso_trans A B C R S T: oiso A B R S -> oiso A C R T -> oiso B C S T.

Corollary ordiso_trans A B R a: ordiso A a R -> ordiso B a R -> oiso A B R R.

Lemma image_oisomorph f A B A' R S: oisomorphism f A B R S -> A' c= A
  -> oisomorphism (f|A') A' (f[(A')]) R (S|> (f[(A')])).

Lemma image_oisomorph2 f A B A' R S: oisomorphism f A B R S -> A' c= A
  -> oisomorphism (f|A') A' (f|A'[(A')]) R (S|> (f|A'[(A')])).

Lemma res_oisomorph f A B R S: oisomorphism f A B R S -> oisomorphism f A B (R|>A) S.

Lemma oiso_iseg f M a R b: oisomorphism f M a R (elorder a) -> ordinal a -> b <e a
  -> b = f[(iseg M R (f^[b]))].

Lemma oiso_images f a b x: ordinal a -> ordinal b -> x <e a ->
  oisomorphism f a b (elorder a) (elorder b) -> (forall c : set, c <e x -> (c, c) <e f) ->
  f[x] = f[(x)].

Lemma oiso_eq f A B R S x: oisomorphism f A B R S -> x <e A
  -> iseg B S (f[x]) = f[(iseg A R x)].