Library ZFrepl

Require Import ZF.

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) :=
  (∀ x x' y y', x ∈ a -> x == x' -> y == y' -> R x y -> R x' y') /\
  (∀ x y y', x ∈ a -> R x y -> R x y' -> y == y').

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

Lemma repl_intro : ∀ a R y x,
  repl_rel a R -> y ∈ a -> R y x -> x ∈ repl a R.

Lemma repl_elim : ∀ a R x,
  repl_rel a R -> x ∈ repl a R -> exists2 y, y ∈ a & R y x.

Lemma repl_ext : ∀ p a R,
  repl_rel a R ->
  (∀ x y, x ∈ a -> R x y -> y ∈ p) ->
  (∀ y, y ∈ p -> exists2 x, x ∈ a & R x y) ->
  p == repl a R.

Lemma repl_mono2 : ∀ x y R,
  repl_rel y R ->
  x ⊆ y ->
  repl x R ⊆ repl y R.

Lemma repl_empty : ∀ 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) :=
  (∀ x x', x == x' -> P x -> P x') /\
  (exists x, P x) /\
  (∀ x x', P x -> P x' -> x == x').

Instance uchoice_pred_morph : Proper ((eq_set ==> iff) ==> iff) uchoice_pred.


Qed.

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

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

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

Lemma uchoice_ax : ∀ P x,
  uchoice_pred P ->
  (x ∈ uchoice P <-> exists2 z, P z & x ∈ z).