Require Export Definability.

Class ZF_Operations (S : ZF_Structure) :=
  build_zf_operations {
      empty_set : S;
      unordered_pair : S → S → S;
      power_set : S → S;
      big_union : S → S;
      infinite_set : S;
      relation_replacement:
        ∀ R : S → S → Prop,
          Is_Definable R →
          Is_Functional R →
          S →
          S
    }.

Notation "∅" := empty_set.
Notation "`{ u , v }" :=
  (unordered_pair u v)
    (at level 9, u at level 69, v at level 69, format "`{ u , v }").
Notation 𝒫 := power_set.
Notation "`{ u }" := (`{u, u})
                       (at level 9, u at level 69, format "`{ u }").
Notation "A ∪ B" := (big_union `{A, B}) (at level 50).

Class ZF_Model :=
  build_zf_model {

      zf_structure :> ZF_Structure;
      zf_operations :> ZF_Operations zf_structure;


      extensionality : ∀ A B : zf_structure, (∀ x, x ∈ A ↔ x ∈ B) → A = B;

      

      foundation : Is_Well_Founded element_relation_on_sets;

      not_in_empty_set :
        ∀ x, x ∉ ∅;

      in_unordered_pair_iff :
        ∀ x y z, z ∈ `{x, y} ↔ z = x ∨ z = y;

      in_power_set_iff :
        ∀ A x, x ∈ 𝒫 A ↔ x ⊆ A;

      in_big_union_iff :
        ∀ A x, x ∈ big_union A ↔ ∃ B : A, x ∈ B;

      infinite_set_property :
        ∅ ∈ infinite_set ∧
        ∀ x : infinite_set, x ∪ `{x} ∈ infinite_set;

      in_relation_replacement_iff :
        ∀ R definable functional A y,
          y ∈ relation_replacement R definable functional A ↔ ∃ x : A, R x y

    }.

Coercion zf_structure : ZF_Model >-> ZF_Structure.