# Library ZFdef

Require Export Setoid.

Module Type IZF_sig.

Parameter
(set : Type)
(empty : set)
(pair : set -> set -> set)
(union : set -> set)
(infinite : set)
(power : set -> set)
(repl : set -> (set -> set -> Prop) -> set)
(eq_set : set -> set -> Prop)
(in_set : set -> set -> Prop).

Notation "x \in y" := (in_set x y) (at level 60).
Notation "x == y" := (eq_set x y) (at level 70).

Parameter
(eq_set_ax : forall a b, a == b <-> (forall x, x \in a <-> x \in b))
(in_reg : forall a a' b, a == a' -> a \in b -> a' \in b)

(empty_ax: forall x, ~ x \in empty)
(pair_ax: forall a b x, x \in pair a b <-> (x == a \/ x == b))
(union_ax: forall a x, x \in union a <-> (exists2 y, x \in y & y \in a))
(infinity_ax1: empty \in infinite)
(infinity_ax2: forall x,
x \in infinite -> union (pair x (pair x x)) \in infinite)
(power_ax: forall a x, x \in power a <-> (forall y, y \in x -> y \in a))
(repl_mono: forall a a',
(forall z, z \in a -> z \in a') ->
forall (R R':set->set->Prop),
(forall x x', x==x' -> forall y y', y==y' -> (R x y <-> R' x' y')) ->
forall z, z \in repl a R -> z \in repl a' R')
(repl_ax:
forall a (R:set->set->Prop),
(forall x x' y y', x \in a -> R x y -> R x' y' -> x == x' -> y == y') ->
forall x, x \in repl a R <-> (exists2 y, y \in a & exists2 x', x == x' & R y x'))
(regularity_ax: forall a a0, a0 \in a ->
exists2 b, b \in a & ~(exists2 c, c \in a & c \in b)).

End IZF_sig.

Module Type IZF_Ex_sig.

Parameter
(set : Type)
(eq_set : set -> set -> Prop)
(in_set : set -> set -> Prop).

Notation "x \in y" := (in_set x y) (at level 60).
Notation "x == y" := (eq_set x y) (at level 70).

Parameter
(eq_set_ax : forall a b, a == b <-> (forall x, x \in a <-> x \in b))
(in_reg : forall a a' b, a == a' -> a \in b -> a' \in b)

(empty_ex: exists empty, forall x, ~ x \in empty)
(pair_ex: forall a b, exists c, forall x, x \in c <-> (x == a \/ x == b))
(union_ex: forall a, exists b,
forall x, x \in b <-> (exists2 y, x \in y & y \in a))
(infinity_ex: exists2 infinite,
(exists2 empty, (forall x, ~ x \in empty) & empty \in infinite) &
(forall x, x \in infinite ->
exists2 y, (forall z, z \in y <-> (z == x \/ z \in x)) &
y \in infinite))
(power_ex: forall a, exists b,
forall x, x \in b <-> (forall y, y \in x -> y \in a))
(repl_ex:
forall a (R:set->set->Prop),
(forall x x' y y', x \in a -> R x y -> R x' y' -> x == x' -> y == y') ->
exists b, forall x, x \in b <-> (exists2 y, y \in a & exists2 x', x == x' & R y x'))
(regularity_ax: forall a a0, a0 \in a ->
exists2 b, b \in a & ~(exists2 c, c \in a & c \in b)).

End IZF_Ex_sig.