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