Library ZF

Require Export Setoid Morphisms.
Require Export ZFdef.

Require Ens ZFskol.
Module IZF : IZF_sig := ZFskol.Skolem Ens.IZF.
Import IZF.

Notation morph1 := (Proper (eq_set ==> eq_set)).
Notation morph2 := (Proper (eq_set ==> eq_set ==> eq_set)).

Instance eq_set_equiv: Equivalence eq_set.

Lemma eq_intro : forall x y,
  (forall z, z \in x -> z \in y) ->
  (forall z, z \in y -> z \in x) ->
  eq_set x y.

Lemma eq_elim : forall x y y',
  y == y' ->
  x \in y ->
  x \in y'.

Instance in_set_morph : Proper (eq_set ==> eq_set ==> iff) in_set.

Qed.

Definition incl_set x y := forall z, z \in x -> z \in y.

Notation "x \incl y" := (incl_set x y) (at level 70).

Instance incl_set_pre : PreOrder incl_set.
Qed.

Instance incl_set_morph : Proper (eq_set ==> eq_set ==> iff) incl_set.
Qed.

Lemma incl_eq : forall x y, x \incl y -> y \incl x -> x == y.


Definition eq_fun dom F G :=
  forall x x', x \in dom -> x == x' -> F x == G x'.

Instance eq_fun_sym : forall dom, Symmetric (eq_fun dom).
Qed.

Instance eq_fun_trans : forall dom, Transitive (eq_fun dom).
Qed.

Definition ext_fun dom f := eq_fun dom f f.

Lemma eq_fun_ext : forall dom F G, eq_fun dom F G -> ext_fun dom F.

Definition eq_pred dom (P Q : set -> Prop) :=
  forall x, x \in dom -> (P x <-> Q x).

Instance eq_pred_set : forall dom, Equivalence (eq_pred dom).
Qed.

Definition ext_rel dom (R:set->set->Prop) :=
  forall x x' y y', x \in dom -> x == x' -> y == y' -> (R x y <-> R x' y').

Definition eq_index x F y G :=
  (forall a, a \in x -> exists2 b, b \in y & F a == G b) /\
  (forall b, b \in y -> exists2 a, a \in x & F a == G b).

Lemma eq_index_sym : forall x F y G, eq_index x F y G -> eq_index y G x F.

Lemma eq_index_eq : forall x F y G,
  x == y ->
  eq_fun x F G ->
  eq_index x F y G.


Definition subset a (P:set->Prop) := repl a (fun x y => x==y /\ P x).

Lemma subset_ax: forall a (P:set->Prop),
    forall x, x \in subset a P <-> (x \in a /\ exists2 x', x==x' & P x').


Lemma empty_ext : forall e, (forall x, ~x \in e) -> e == empty.

Lemma pair_intro1 : forall x y, x \in pair x y.

Lemma pair_intro2 : forall x y, y \in pair x y.

Hint Resolve pair_intro1 pair_intro2.

Lemma pair_elim : forall x a b, x \in pair a b -> x == a \/ x == b.

Lemma pair_ext : forall p a b,
  a \in p -> b \in p -> (forall x, x \in p -> x == a \/ x == b) ->
  p == pair a b.

Instance pair_morph : morph2 pair.

Qed.

Lemma union_intro : forall x y z, x \in y -> y \in z -> x \in union z.

Lemma union_elim : forall x z, x \in union z -> exists2 y, x \in y & y \in z.

Lemma union_ext :
  forall u z,
  (forall x y, x \in y -> y \in z -> x \in u) ->
  (forall x, x \in u -> exists2 y, x \in y & y \in z) ->
  u == union z.

Instance union_morph : morph1 union.
Qed.

Lemma union_empty_eq : union empty == empty.

Lemma power_intro :
  forall x y, (forall z, z \in x -> z \in y) -> x \in power y.

Lemma power_elim : forall x y z, x \in power y -> z \in x -> z \in y.

Lemma power_mono : Proper (incl_set ==> incl_set) power.

Lemma power_ext :
  forall p a,
  (forall x, (forall y, y \in x -> y \in a) -> x \in p) ->
  (forall x y, x \in p -> y \in x -> y \in a) ->
  p == power a.

Instance power_morph : morph1 power.
Qed.

Lemma empty_in_power : forall x, empty \in power x.

Lemma union_in_power :
    forall x X, x \incl power X -> union x \in power X.

Lemma subset_intro : forall a (P:set->Prop) x,
  x \in a -> P x -> x \in subset a P.

Lemma subset_elim1 : forall a (P:set->Prop) x, x \in subset a P -> x \in a.

Lemma subset_elim2 : forall a (P:set->Prop) x, x \in subset a P ->
  exists2 x', x==x' & P x'.

Lemma subset_ext :
  forall s a (P:set->Prop),
  (forall x, x \in a -> P x -> x \in s) ->
  (forall x, x \in s -> x \in a) ->
  (forall x, x \in s -> exists2 x', x==x' & P x') ->
  s == subset a P.

Lemma subset_morph :
  forall x x', x == x' ->
  forall (P P':set->Prop), eq_pred x P P' ->
  subset x P == subset x' P'.

Lemma union_subset_singl : forall x (P:set->Prop) y y',
  y \in x ->
  y == y' ->
  P y' ->
  (forall y y', y \in x -> y' \in x -> P y -> P y' -> y == y') ->
  union (subset x P) == y.

Definition replf a (F:set->set) :=
  repl a (fun x y => y == F x).

Instance replf_mono_raw :
  Proper (incl_set ==> (eq_set ==> eq_set) ==> incl_set) replf.
Qed.

Instance replf_morph_raw :
  Proper (eq_set ==> (eq_set ==> eq_set) ==> eq_set) replf.

Qed.

Lemma replf_ax : forall a F z,
  ext_fun a F ->
  (z \in replf a F <-> exists2 x, x \in a & z == F x).

Lemma replf_intro : forall a F y x,
  ext_fun a F -> x \in a -> y == F x -> y \in replf a F.

Lemma replf_elim : forall a F y,
  ext_fun a F -> y \in replf a F -> exists2 x, x \in a & y == F x.

Lemma replf_ext : forall p a F,
  ext_fun a F ->
  (forall x, x \in a -> F x \in p) ->
  (forall y, y \in p -> exists2 x, x \in a & y == F x) ->
  p == replf a F.

Lemma replf_mono2 : forall x y F,
  ext_fun y F ->
  x \incl y ->
  replf x F \incl replf y F.

Lemma replf_morph_gen : forall x1 x2 F1 F2,
  ext_fun x1 F1 ->
  ext_fun x2 F2 ->
  eq_index x1 F1 x2 F2 ->
  replf x1 F1 == replf x2 F2.

Lemma replf_morph : forall x1 x2 F1 F2,
  x1 == x2 ->
  eq_fun x1 F1 F2 ->
  replf x1 F1 == replf x2 F2.

Lemma replf_empty : forall F, replf empty F == empty.


Lemma pair_commut : forall x y, pair x y == pair y x.

Lemma pair_inv : forall x y x' y',
  pair x y == pair x' y' -> (x==x' /\ y==y') \/ (x==y' /\ y==x').

Definition singl x := pair x x.

Lemma singl_intro : forall x, x \in singl x.

Lemma singl_intro_eq : forall x y, x == y -> x \in singl y.

Lemma singl_elim : forall x y, x \in singl y -> x == y.

Lemma singl_ext :
  forall y x,
  x \in y ->
  (forall z, z \in y -> z == x) ->
  y == singl x.

Instance singl_morph : morph1 singl.
Qed.

Lemma union_singl_eq : forall x, union (singl x) == x.

Lemma singl_inj : forall x y, singl x == singl y -> x == y.

Definition union2 x y := union (pair x y).

Lemma union2_intro1: forall x y z, z \in x -> z \in union2 x y.

Lemma union2_intro2: forall x y z, z \in y -> z \in union2 x y.

Lemma union2_elim : forall x y z, z \in union2 x y -> z \in x \/ z \in y.

Lemma union2_mono : forall A A' B B',
  A \incl A' -> B \incl B' -> union2 A B \incl union2 A' B'.

Instance union2_morph : morph2 union2.
Qed.

Lemma union2_commut : forall x y, union2 x y == union2 y x.

Definition minus2 x y := subset x (fun x' => ~ (x' \in y)).


Definition sup x F := union (replf x F).

Lemma sup_ax : forall x F z,
  ext_fun x F ->
  (z \in sup x F <-> exists2 y, y \in x & z \in F y).

Lemma sup_ext : forall y a F,
  ext_fun a F ->
  (forall x, x \in a -> F x \incl y) ->
  (forall z, z \in y -> exists2 x, x \in a & z \in F x) ->
  y == sup a F.

Lemma sup_morph_gen : forall a F b G,
  ext_fun a F ->
  ext_fun b G ->
  eq_index a F b G ->
  sup a F == sup b G.

Lemma sup_morph : forall a F b G,
  a == b ->
  eq_fun a F G ->
  sup a F == sup b G.

Lemma sup_incl : forall a F x,
  ext_fun a F -> x \in a -> F x \incl sup a F.
Hint Resolve sup_incl.


Section Russel.

Variable U : set.
Variable universal : forall x, x \in U.

Definition omega := subset U (fun x => ~ x \in x).

Lemma omega_not_in_omega : ~ omega \in omega.

Lemma omega_in_omega : omega \in omega.

Lemma no_universal_set : False.
End Russel.


Definition inter x := subset (union x) (fun y => forall z, z \in x -> y \in z).

Lemma inter_empty_eq : inter empty == empty.

Lemma inter_intro :
  forall x a y0,
  (forall y, y \in a -> x \in y) ->
  y0 \in a ->
  x \in inter a.

Lemma inter_elim : forall x a y, x \in inter a -> y \in a -> x \in y.

Lemma inter_ext :
  forall i a y0,
  (forall y, y \in a -> i \incl y) ->
  (forall x, (forall y, y \in a -> x \in y) -> x \in i) ->
  y0 \in a ->
  i == inter a.

Instance inter_morph : morph1 inter.

Qed.