Library ZFpairs

Require Export ZF.



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

Instance couple_morph : morph2 couple.
Qed.

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

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

Instance fst_morph : morph1 fst.
Qed.

Lemma fst_def : ∀ 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 : ∀ x y, snd (couple x y) == y.

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


Definition prodcart A B :=
  subset (power (power (A ∪ B)))
    (fun x => exists2 a, a ∈ A & exists2 b, b ∈ 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 :
  ∀ x y A B, x ∈ A -> y ∈ B -> couple x y ∈ prodcart A B.

Lemma fst_typ : ∀ p A B, p ∈ prodcart A B -> fst p ∈ A.

Lemma snd_typ : ∀ p A B, p ∈ prodcart A B -> snd p ∈ B.

Lemma surj_pair :
  ∀ p A B, p ∈ prodcart A B -> p == couple (fst p) (snd p).


Definition sigma A B :=
  subset (prodcart A (sup A B)) (fun p => snd p ∈ B (fst p)).

Instance sigma_morph : Proper (eq_set ==> (eq_set ==> eq_set) ==> eq_set) sigma.

Qed.

Lemma sigma_ext : ∀ A A' B B',
  A == A' ->
  (∀ x x', x ∈ A -> x == x' -> B x == B' x') ->
  sigma A B == sigma A' B'.

Lemma sigma_nodep : ∀ A B,
  prodcart A B == sigma A (fun _ => B).

Lemma couple_intro_sigma :
  ∀ x y A B,
  ext_fun A B ->
  x ∈ A -> y ∈ B x -> couple x y ∈ sigma A B.

Lemma fst_typ_sigma : ∀ p A B, p ∈ sigma A B -> fst p ∈ A.

Lemma snd_typ_sigma : ∀ p y A B,
  ext_fun A B ->
  p ∈ sigma A B -> y == fst p -> snd p ∈ B y.

Lemma sigma_mono : ∀ A A' B B',
  ext_fun A B ->
  ext_fun A' B' ->
  A ⊆ A' ->
  (∀ x x', x ∈ A -> x == x' -> B x ⊆ B' x') ->
  sigma A B ⊆ sigma A' B'.