Library ZF

Require Export basic.
Require Import Sublogic.
Require Export ZFdef.

Require ZFskolEm.
Module IZF : IZF_R_sig CoqSublogicThms := ZFskolEm.IZF_R.
Include 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 : ∀ x y,
  (∀ z, z ∈ x -> z ∈ y) ->
  (∀ z, z ∈ y -> z ∈ x) ->
  eq_set x y.

Lemma eq_elim : ∀ x y y',
  y == y' ->
  x ∈ y ->
  x ∈ y'.

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

Definition incl_set x y := ∀ z, z ∈ x -> z ∈ y.

Notation "x ⊆ y" := (incl_set x y).

Instance incl_set_pre : PreOrder incl_set.
Qed.

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

Lemma incl_eq : ∀ x y, x ⊆ y -> y ⊆ x -> x == y.

Instance Fmono_morph F : Proper (incl_set==>incl_set) F -> morph1 F.
Qed.
Hint Resolve Fmono_morph.

Definition eq_fun dom F G :=
  ∀ x x', x ∈ dom -> x == x' -> F x == G x'.

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

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

Definition ext_fun dom f := eq_fun dom f f.

Definition ext_fun2 A B f :=
  ∀ x x' y y', x ∈ A -> x == x' -> y ∈ B x -> y == y' -> f x y == f x' y'.

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

Lemma morph_is_ext : ∀ F X, morph1 F -> ext_fun X F.
Hint Resolve morph_is_ext.

Definition eq_pred dom (P Q : set -> Prop) :=
  ∀ x, x ∈ dom -> (P x <-> Q x).

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

Definition ext_rel dom (R:set->set->Prop) :=
  ∀ x x' y y', x ∈ dom -> x == x' -> y == y' -> (R x y <-> R x' y').

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

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

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

Definition typ_fun f A B := ∀ x, x ∈ A -> f x ∈ B.

Instance typ_fun_morph0 : Proper (eq ==> eq_set ==> eq_set ==> iff) typ_fun.
Qed.

Lemma empty_ext : ∀ e, (∀ x, ~x ∈ e) -> e == empty.

Lemma pair_intro1 : ∀ x y, x ∈ pair x y.

Lemma pair_intro2 : ∀ x y, y ∈ pair x y.

Hint Resolve pair_intro1 pair_intro2.

Lemma pair_elim : ∀ x a b, x ∈ pair a b -> x == a \/ x == b.

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

Instance pair_morph : morph2 pair.

Qed.

Lemma union_intro : ∀ x y z, x ∈ y -> y ∈ z -> x ∈ union z.

Lemma union_elim : ∀ x z, x ∈ union z -> exists2 y, x ∈ y & y ∈ z.

Lemma union_ext :
  ∀ u z,
  (∀ x y, x ∈ y -> y ∈ z -> x ∈ u) ->
  (∀ x, x ∈ u -> exists2 y, x ∈ y & y ∈ z) ->
  u == union z.

Instance union_morph : morph1 union.
Qed.

Instance union_mono : Proper (incl_set ==> incl_set) union.
Qed.

Lemma union_empty_eq : union empty == empty.

Lemma power_intro :
  ∀ x y, (∀ z, z ∈ x -> z ∈ y) -> x ∈ power y.

Lemma power_elim : ∀ x y z, x ∈ power y -> z ∈ x -> z ∈ y.

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

Lemma power_ext :
  ∀ p a,
  (∀ x, (∀ y, y ∈ x -> y ∈ a) -> x ∈ p) ->
  (∀ x y, x ∈ p -> y ∈ x -> y ∈ a) ->
  p == power a.

Instance power_morph : morph1 power.
Qed.

Lemma empty_in_power : ∀ x, empty ∈ power x.

Lemma union_in_power :
    ∀ x X, x ⊆ power X -> union x ∈ power X.

Lemma subset_intro : ∀ a (P:set->Prop) x,
  x ∈ a -> P x -> x ∈ subset a P.

Lemma subset_elim1 : ∀ a (P:set->Prop) x, x ∈ subset a P -> x ∈ a.

Lemma subset_elim2 : ∀ a (P:set->Prop) x, x ∈ subset a P ->
  exists2 x', x==x' & P x'.

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

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

Lemma union_subset_singl : ∀ x (P:set->Prop) y y',
  y ∈ x ->
  y == y' ->
  P y' ->
  (∀ y y', y ∈ x -> y' ∈ 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 : ∀ a F z,
  ext_fun a F ->
  (z ∈ replf a F <-> exists2 x, x ∈ a & z == F x).

Lemma replf_intro : ∀ a F y x,
  ext_fun a F -> x ∈ a -> y == F x -> y ∈ replf a F.

Lemma replf_elim : ∀ a F y,
  ext_fun a F -> y ∈ replf a F -> exists2 x, x ∈ a & y == F x.

Lemma replf_ext : ∀ p a F,
  ext_fun a F ->
  (∀ x, x ∈ a -> F x ∈ p) ->
  (∀ y, y ∈ p -> exists2 x, x ∈ a & y == F x) ->
  p == replf a F.

Lemma replf_mono2 : ∀ x y F,
  ext_fun y F ->
  x ⊆ y ->
  replf x F ⊆ replf y F.

Lemma replf_morph_gen : ∀ 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 : ∀ x1 x2 F1 F2,
  x1 == x2 ->
  eq_fun x1 F1 F2 ->
  replf x1 F1 == replf x2 F2.

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

Lemma compose_replf : ∀ A F G,
  ext_fun A F ->
  ext_fun (replf A F) G ->
  replf (replf A F) G == replf A (fun x => G (F x)).

  Definition cond_set P x := subset x (fun _ => P).

  Instance cond_set_morph : Proper (iff ==> eq_set ==> eq_set) cond_set.
Qed.

  Lemma cond_set_ax P x z :
    z ∈ cond_set P x <-> (z ∈ x /\ P).

 Lemma cond_set_morph2 : ∀ P Q x y,
    (P <-> Q) ->
    (P -> x == y) ->
    cond_set P x == cond_set Q y.

  Lemma cond_set_ok (P:Prop) x : P -> cond_set P x == x.

  Lemma cond_set_elim_prop x P z : z ∈ cond_set P x -> P.

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

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

Lemma discr_mt_pair : ∀ a b, ~ empty == pair a b.

Definition singl x := pair x x.

Lemma singl_intro : ∀ x, x ∈ singl x.

Lemma singl_intro_eq : ∀ x y, x == y -> x ∈ singl y.

Lemma singl_elim : ∀ x y, x ∈ singl y -> x == y.

Lemma singl_ext :
  ∀ y x,
  x ∈ y ->
  (∀ z, z ∈ y -> z == x) ->
  y == singl x.

Instance singl_morph : morph1 singl.
Qed.

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

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

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

Infix "∪" := union2.

Lemma union2_intro1: ∀ x y z, z ∈ x -> z ∈ union2 x y.

Lemma union2_intro2: ∀ x y z, z ∈ y -> z ∈ union2 x y.

Lemma union2_elim : ∀ x y z, z ∈ x ∪ y -> z ∈ x \/ z ∈ y.

Lemma union2_ax x y z : z ∈ x ∪ y <-> z ∈ x \/ z ∈ y.

Lemma union2_mono : ∀ A A' B B',
  A ⊆ A' -> B ⊆ B' -> A ∪ B ⊆ A' ∪ B'.

Instance union2_morph : morph2 union2.
Qed.

Lemma union2_commut : ∀ x y, x ∪ y == y ∪ x.

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

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

Lemma sup_ax : ∀ x F z,
  ext_fun x F ->
  (z ∈ sup x F <-> exists2 y, y ∈ x & z ∈ F y).

Lemma sup_ext : ∀ y a F,
  ext_fun a F ->
  (∀ x, x ∈ a -> F x ⊆ y) ->
  (∀ z, z ∈ y -> exists2 x, x ∈ a & z ∈ F x) ->
  y == sup a F.

Lemma sup_morph_gen : ∀ 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 : ∀ a F b G,
  a == b ->
  eq_fun a F G ->
  sup a F == sup b G.

Lemma sup_incl : ∀ a F x,
  ext_fun a F -> x ∈ a -> F x ⊆ sup a F.
Hint Resolve sup_incl.

Lemma replf_is_sup A F :
  ext_fun A F ->
  replf A F == sup A (fun x => singl (F x)).

Lemma union_is_sup a :
  union a == sup a (fun x => x).

Section Russel.

Variable U : set.
Variable universal : ∀ x, x ∈ U.

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

Lemma omega_not_in_omega : ~ omega ∈ omega.

Lemma omega_in_omega : omega ∈ omega.

Lemma no_universal_set : False.
End Russel.

Definition inter x := subset (union x) (fun y => ∀ z, z ∈ x -> y ∈ z).

Lemma inter_empty_eq : inter empty == empty.

Lemma inter_intro :
  ∀ x a,
  (∀ y, y ∈ a -> x ∈ y) ->
  (exists w, w ∈ a) ->
  x ∈ inter a.

Lemma inter_elim : ∀ x a y, x ∈ inter a -> y ∈ a -> x ∈ y.

Lemma inter_non_empty :
  ∀ x y, y ∈ inter x -> exists2 w, w ∈ x & y ∈ w.

Lemma inter_wit : ∀ X F, morph1 F ->
 ∀ x, x ∈ inter (replf X F) ->
 exists y, y ∈ X.

Lemma inter_ext :
  ∀ i a,
  (∀ y, y ∈ a -> i ⊆ y) ->
  (∀ x, (∀ y, y ∈ a -> x ∈ y) -> x ∈ i) ->
  (exists w, w ∈ a) ->
  i == inter a.

Instance inter_morph : morph1 inter.

Qed.

Definition inter2 x y := inter (pair x y).

Infix "∩" := inter2.

Instance inter2_morph: morph2 inter2.
Qed.

Lemma inter2_def : ∀ x y z,
  z ∈ x ∩ y <-> z ∈ x /\ z ∈ y.

Lemma inter2_incl1 : ∀ x y, x ∩ y ⊆ x.

Lemma inter2_incl2 : ∀ x y, x ∩ y ⊆ y.

Lemma inter2_incl a x y : a ⊆ x -> a ⊆ y -> a ⊆ x ∩ y.

Lemma incl_inter2 x y: x ⊆ y -> x ∩ y == x.

Lemma inter2_comm x y :
  x ∩ y == y ∩ x.