# 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.