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.