Library ZFpairs


Require Export ZF.
Import IZF.



Definition couple x y := pair (singl x) (pair x y).

Instance couple_morph : morph2 couple.
Qed.

Lemma union_couple_eq : forall a b, union (couple a b) == pair a b.

Definition fst p := union (subset (union p) (fun x => singl x \in p)).

Instance fst_morph : morph1 fst.
Qed.

Lemma fst_def : forall x y, fst (couple x y) == x.

Definition snd p :=
  union (subset (union p) (fun z => pair (fst p) z == union p)).

Instance snd_morph : morph1 snd.

Lemma snd_def : forall x y, snd (couple x y) == y.

Lemma couple_injection : forall x y x' y',
  couple x y == couple x' y' -> x == x' /\ y == y'.


Definition prodcart A B :=
  subset (power (power (union2 A B)))
    (fun x => exists2 a, a \in A & exists2 b, b \in B & x == couple a b).

Instance prodcart_mono :
  Proper (incl_set ==> incl_set ==> incl_set) prodcart.

Qed.

Instance prodcart_morph : morph2 prodcart.

Lemma couple_intro :
  forall x y A B, x \in A -> y \in B -> couple x y \in prodcart A B.

Lemma fst_typ : forall p A B, p \in prodcart A B -> fst p \in A.

Lemma snd_typ : forall p A B, p \in prodcart A B -> snd p \in B.

Lemma surj_pair :
  forall p A B, p \in prodcart A B -> p == couple (fst p) (snd p).


Definition sigma A B :=
  subset (prodcart A (union (replf A B)))
    (fun p => snd p \in B (fst p)).

Lemma sigma_morph : forall A A' B B',
  A == A' ->
  (forall x x', x \in A -> x == x' -> B x == B' x') ->
  sigma A B == sigma A' B'.

Lemma couple_intro_sigma :
  forall x y A B,
  ext_fun A B ->
  x \in A -> y \in B x -> couple x y \in sigma A B.

Lemma fst_typ_sigma : forall p A B, p \in sigma A B -> fst p \in A.

Lemma snd_typ_sigma : forall p y A B,
  ext_fun A B ->
  p \in sigma A B -> y == fst p -> snd p \in B y.