Library ZFrepl

Require Export ZF.
Import IZF.

Instance repl_mono_raw :
  Proper (incl_set ==> (eq_set ==> eq_set ==> iff) ==> incl_set) repl.

Instance repl_morph_raw :
  Proper (eq_set ==> (eq_set ==> eq_set ==> iff) ==> eq_set) repl.

Qed.

Definition repl_rel a (R:set->set->Prop) :=
  (forall x x' y y', x \in a -> x == x' -> y == y' -> R x y -> R x' y') /\
  (forall x y y', x \in a -> R x y -> R x y' -> y == y').
Lemma repl_rel_compat_lemma : forall a R,
  repl_rel a R ->
  (forall x x' y y', x \in a -> R x y -> R x' y' -> x == x' -> y == y').

Lemma repl_rel_fun : forall x f,
  ext_fun x f -> repl_rel x (fun a b => b == f a).

Lemma repl_intro : forall a R y x,
  repl_rel a R -> y \in a -> R y x -> x \in repl a R.

Lemma repl_elim : forall a R x,
  repl_rel a R -> x \in repl a R -> exists2 y, y \in a & R y x.

Lemma repl_ext : forall p a R,
  repl_rel a R ->
  (forall x y, x \in a -> R x y -> y \in p) ->
  (forall y, y \in p -> exists2 x, x \in a & R x y) ->
  p == repl a R.

Lemma repl_mono2 : forall x y R,
  repl_rel y R ->
  x \incl y ->
  repl x R \incl repl y R.

Lemma repl_empty : forall R, repl empty R == empty.

Definition uchoice (P : set -> Prop) : set :=
  union (repl (singl empty) (fun _ => P)).

Instance uchoice_morph_raw : Proper ((eq_set ==> iff) ==> eq_set) uchoice.
Qed.

Definition uchoice_pred (P:set->Prop) :=
  (forall x x', x == x' -> P x -> P x') /\
  (exists x, P x) /\
  (forall x x', P x -> P x' -> x == x').

Lemma uchoice_ext : forall P x, uchoice_pred P -> P x -> x == uchoice P.

Lemma uchoice_def : forall P, uchoice_pred P -> P (uchoice P).

Lemma uchoice_morph : forall P P',
  uchoice_pred P ->
  (forall x, P x <-> P' x) ->
  uchoice P == uchoice P'.

Lemma uchoice_ax : forall P x,
  uchoice_pred P ->
  (x \in uchoice P <-> exists2 z, P z & x \in z).