Library ZFgrothendieck

Require Import ZF.
Require Import ZFpairs ZFrelations ZFrepl.
Import IZF.

Record grot_univ (U:set) : Prop := {
  G_trans : forall x y, y \in x -> x \in U -> y \in U;
  G_pair : forall x y, x \in U -> y \in U -> pair x y \in U;
  G_power : forall x, x \in U -> power x \in U;
  G_union_repl : forall I R, repl_rel I R -> I \in U ->
                (forall x y, x \in I -> R x y -> y \in U) ->
                union (repl I R) \in U }.

Lemma grot_univ_ext : forall U U',
  U == U' -> grot_univ U -> grot_univ U'.

Lemma grot_empty : grot_univ empty.


Section GrothendieckUniverse.

Variable U : set.
Hypothesis grot : grot_univ U.

Lemma G_subset : forall x P, x \in U -> subset x P \in U.

Lemma G_singl : forall x, x \in U -> singl x \in U.

Lemma G_repl : forall A R,
  repl_rel A R ->
  A \in U ->
  (forall x y, x \in A -> R x y -> y \in U) ->
  repl A R \in U.

Lemma G_union : forall x, x \in U -> union x \in U.

Lemma G_replf : forall A F,
  ext_fun A F ->
  A \in U ->
  (forall x, x \in A -> F x \in U) ->
  replf A F \in U.

Lemma G_union2 : forall x y, x \in U -> y \in U -> union2 x y \in U.

Lemma G_prodcart : forall A B, A \in U -> B \in U -> prodcart A B \in U.

Lemma G_couple : forall x y, x \in U -> y \in U -> couple x y \in U.

Lemma G_rel : forall A B, A \in U -> B \in U -> rel A B \in U.

Lemma G_func : forall A B, A \in U -> B \in U -> func A B \in U.

Lemma G_dep_func : forall X Y,
  ext_fun X Y ->
  X \in U ->
  (forall x, x \in X -> Y x \in U) ->
  dep_func X Y \in U.

End GrothendieckUniverse.

Lemma grot_inter : forall UU,
  (exists x, x \in UU) ->
  (forall x, x \in UU -> grot_univ x) ->
  grot_univ (inter UU).

Lemma grot_intersection : forall (P:set->Prop) x,
  grot_univ x -> P x ->
  grot_univ (subset x (fun y => forall U, grot_univ U -> P U -> y \in U)).

Definition grot_succ_pred x y :=
  grot_univ y /\ x \in y /\ forall U, grot_univ U -> x \in U -> y \incl U.

Definition grothendieck := forall x, exists2 U, grot_univ U & x \in U.

Section TarskiGrothendieck.

Variable gr : grothendieck.

Lemma grot_inter_unique : forall x, uchoice_pred (grot_succ_pred x).

Definition grot_succ U := uchoice (grot_succ_pred U).

Lemma grot_succ_typ : forall x, grot_univ (grot_succ x).

Lemma grot_succ_in : forall x, x \in grot_succ x.

End TarskiGrothendieck.