Library ZFgrothendieck
Require Import ZF.
Require Import ZFpairs ZFsum ZFrelations ZFrepl ZFwf ZFord ZFfix.
Require Import ZFstable.
Require Import ZFlist.
Record grot_univ (U:set) : Prop := {
G_trans : ∀ x y, y ∈ x -> x ∈ U -> y ∈ U;
G_pair : ∀ x y, x ∈ U -> y ∈ U -> pair x y ∈ U;
G_power : ∀ x, x ∈ U -> power x ∈ U;
G_union_repl : ∀ I R, repl_rel I R -> I ∈ U ->
(∀ x y, x ∈ I -> R x y -> y ∈ U) ->
union (repl I R) ∈ U }.
Lemma grot_univ_ext : ∀ U U',
U == U' -> grot_univ U -> grot_univ U'.
destruct 2; split; intros.
rewrite <- H in H1|-*; eauto.
rewrite <- H in H0,H1|-*; auto.
rewrite <- H in H0|-*; auto.
rewrite <- H in H1|-*.
apply G_union_repl0; intros; auto.
rewrite H; eauto.
Qed.
Lemma grot_empty : grot_univ empty.
split; intros.
elim empty_ax with (1:=H0).
elim empty_ax with (1:=H0).
elim empty_ax with (1:=H).
elim empty_ax with (1:=H0).
Qed.
Section GrothendieckUniverse.
Variable U : set.
Hypothesis grot : grot_univ U.
Lemma G_incl : ∀ x y, x ∈ U -> y ⊆ x -> y ∈ U.
intros.
apply G_trans with (power x); trivial.
rewrite power_ax; auto.
apply G_power; trivial.
Qed.
Lemma G_subset : ∀ x P, x ∈ U -> subset x P ∈ U.
intros.
apply G_incl with x; trivial.
red; intros.
apply subset_elim1 in H0; trivial.
Qed.
Lemma G_singl : ∀ x, x ∈ U -> singl x ∈ U.
unfold singl; intros; apply G_pair; auto.
Qed.
Lemma G_repl : ∀ A R,
repl_rel A R ->
A ∈ U ->
(∀ x y, x ∈ A -> R x y -> y ∈ U) ->
repl A R ∈ U.
intros.
assert (repl_rel A (fun x y => exists2 z, R x z & y == singl z)).
destruct H as (Rext,Rfun).
split; intros.
destruct H4.
exists x0.
apply Rext with x x0; auto; try reflexivity.
transitivity y; auto; symmetry; auto.
destruct H2; destruct H3.
rewrite H4; rewrite H5.
apply singl_morph.
eauto.
setoid_replace (repl A R) with
(union (repl A (fun x y => exists2 z, R x z & y == singl z))).
apply G_union_repl; trivial.
destruct 2.
rewrite H5.
apply G_singl; eauto.
apply union_ext; intros.
elim repl_elim with (2:=H4); trivial; intros.
destruct H6.
rewrite H7 in H3.
rewrite (singl_elim _ _ H3).
apply repl_intro with x0; trivial.
elim repl_elim with (2:=H3); trivial; intros.
exists (singl x).
apply singl_intro.
apply repl_intro with x0; trivial.
exists x; trivial; reflexivity.
Qed.
Lemma G_union : ∀ x, x ∈ U -> union x ∈ U.
intros.
setoid_replace x with (repl x (fun y z => z==y)).
apply G_union_repl; trivial; intros.
apply repl_rel_fun with (f:=fun x:set=>x).
do 2 red; auto.
rewrite H1; apply G_trans with x; trivial.
apply repl_ext; intros.
apply repl_rel_fun with (f:=fun x:set=>x).
do 2 red; auto.
rewrite H1; trivial.
exists y; trivial; reflexivity.
Qed.
Lemma G_replf : ∀ A F,
ext_fun A F ->
A ∈ U ->
(∀ x, x ∈ A -> F x ∈ U) ->
replf A F ∈ U.
unfold replf; intros; apply G_repl; intros; auto.
apply repl_rel_fun; trivial.
rewrite H3; auto.
Qed.
Lemma G_union2 : ∀ x y, x ∈ U -> y ∈ U -> x ∪ y ∈ U.
intros.
unfold union2.
apply G_union.
apply G_pair; trivial.
Qed.
Lemma G_sup A B :
ext_fun A B ->
A ∈ U ->
(∀ x, x ∈ A -> B x ∈ U) ->
sup A B ∈ U.
intros.
apply G_union; trivial.
apply G_replf; trivial.
Qed.
Lemma G_nat x : x ∈ U -> ZFnats.N ⊆ U.
red; intros.
elim H0 using ZFnats.N_ind; intros.
rewrite <- H2; trivial.
apply G_incl with x; trivial.
red; intros.
apply empty_ax in H1; contradiction.
apply G_union2; trivial.
apply G_singl; trivial.
Qed.
Lemma G_prodcart : ∀ A B, A ∈ U -> B ∈ U -> prodcart A B ∈ U.
intros.
unfold prodcart.
apply G_subset; intros; trivial.
apply G_power; trivial.
apply G_power; trivial.
apply G_union2; trivial.
Qed.
Lemma G_couple : ∀ x y, x ∈ U -> y ∈ U -> couple x y ∈ U.
intros.
unfold couple.
apply G_pair; trivial.
apply G_singl; trivial.
apply G_pair; trivial.
Qed.
Lemma G_sum X Y : X ∈ U -> Y ∈ U -> sum X Y ∈ U.
unfold sum; intros.
apply G_union2; apply G_prodcart; trivial.
apply G_singl; apply G_nat with X; trivial.
apply ZFnats.zero_typ.
apply G_singl; apply G_nat with X; trivial.
apply ZFnats.succ_typ; apply ZFnats.zero_typ.
Qed.
Lemma G_sumcase A B f g a :
morph1 f ->
morph1 g ->
a ∈ sum A B ->
(∀ a, a ∈ A -> f a ∈ U) ->
(∀ a, a ∈ B -> g a ∈ U) ->
sum_case f g a ∈ U.
intros.
apply sum_case_ind with (6:=H1); intros; auto.
apply morph_impl_iff1; auto with *.
do 3 red; intros.
rewrite <- H4; trivial.
Qed.
Lemma G_rel : ∀ A B, A ∈ U -> B ∈ U -> rel A B ∈ U.
intros.
unfold rel.
apply G_power; trivial.
apply G_prodcart; trivial.
Qed.
Lemma G_func : ∀ A B, A ∈ U -> B ∈ U -> func A B ∈ U.
intros.
unfold func.
apply G_subset; intros; trivial.
apply G_rel; trivial.
Qed.
Lemma G_dep_func : ∀ X Y,
ext_fun X Y ->
X ∈ U ->
(∀ x, x ∈ X -> Y x ∈ U) ->
dep_func X Y ∈ U.
intros.
unfold dep_func.
apply G_subset; intros; trivial.
apply G_func; trivial.
unfold dep_image.
apply G_union; trivial.
apply G_replf; trivial.
Qed.
Lemma G_app f x :
f ∈ U -> x ∈ U -> app f x ∈ U.
unfold app; intros.
apply G_union.
apply G_subset.
unfold rel_image.
apply G_subset.
apply G_union; trivial.
apply G_union; trivial.
Qed.
Lemma G_sigma A B :
ext_fun A B ->
A ∈ U ->
(∀ x, x ∈ A -> B x ∈ U) ->
sigma A B ∈ U.
intros.
apply G_subset; trivial.
apply G_prodcart; trivial.
apply G_sup; trivial.
Qed.
Lemma G_cc_lam A F :
ext_fun A F ->
A ∈ U ->
(∀ x, x ∈ A -> F x ∈ U) ->
cc_lam A F ∈ U.
intros.
unfold cc_lam.
apply G_sup; intros; trivial.
do 2 red; intros; apply replf_morph; auto.
red; intros; apply couple_morph; trivial.
apply G_replf; intros; auto.
do 2 red; intros; apply couple_morph; auto with *.
apply G_couple; trivial.
apply G_trans with A; trivial.
apply G_trans with (F x); auto.
Qed.
Lemma G_cc_app f x :
f ∈ U -> x ∈ U -> cc_app f x ∈ U.
unfold cc_app; intros.
unfold rel_image.
apply G_subset.
apply G_union.
apply G_union.
apply G_subset; trivial.
Qed.
Lemma G_cc_prod A B :
ext_fun A B ->
A ∈ U ->
(∀ x, x ∈ A -> B x ∈ U) ->
cc_prod A B ∈ U.
intros.
unfold cc_prod.
apply G_replf; auto with *.
apply G_dep_func; intros; auto with *.
intros.
apply G_cc_lam; intros; auto.
do 2 red; intros; apply app_morph; auto with *.
apply G_app.
apply G_trans with (dep_func A B); trivial.
apply G_dep_func; trivial.
apply G_trans with A; trivial.
Qed.
Lemma G_TR F o :
Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F ->
(∀ o f f', isOrd o -> eq_fun o f f' -> F f o == F f' o) ->
isOrd o ->
o ∈ U ->
(∀ f o, ext_fun o f -> o ∈ U ->
(∀ o', o' ∈ o -> f o' ∈ U) ->
F f o ∈ U) ->
TR F o ∈ U.
intros Fm Fext oo oU FU.
apply TR_typ with (X:=fun _ => U); auto.
do 2 red; reflexivity.
intros.
apply FU; auto.
apply G_incl with o; trivial.
Qed.
Lemma G_TI F o :
morph1 F ->
isOrd o ->
o ∈ U ->
(∀ x, x ∈ U -> F x ∈ U) ->
TI F o ∈ U.
intros.
apply G_TR; trivial; intros.
do 3 red; intros.
apply sup_morph; auto.
red; intros; auto.
apply sup_morph; auto with *.
red; intros.
apply H; auto.
apply G_sup; auto.
do 2 red; intros; apply H; auto.
Qed.
Lemma G_osup2 x y :
isWf x -> x ∈ U -> y ∈ U -> x ⊔ y ∈ U.
intro wfx; revert y; induction wfx using isWf_ind.
intros.
rewrite osup2_def; trivial.
apply G_union2; trivial.
apply G_union2; trivial.
apply G_union; trivial.
apply G_replf; trivial; intros.
do 2 red; intros; apply replf_morph; auto with *.
red; intros; apply osup2_morph; trivial.
apply G_replf; trivial; intros.
do 2 red; intros; apply osup2_morph; auto with *.
apply H; eauto using G_trans.
Qed.
Lemma G_Ffix F A : A ∈ U -> Ffix F A ∈ U.
intros.
unfold Ffix.
apply G_subset; trivial.
Qed.
Section NonTrivial.
Hypothesis Unontriv : empty ∈ U.
End NonTrivial.
Section Infinite.
Hypothesis Uinf : omega ∈ U.
Lemma G_inf_nontriv : empty ∈ U.
apply G_trans with omega; trivial.
apply zero_omega.
Qed.
Hint Resolve G_inf_nontriv.
Lemma G_List A : A ∈ U -> List A ∈ U.
intros.
unfold List.
apply G_TI; intros; trivial.
apply LISTf_morph.
unfold LISTf.
apply G_union2; trivial.
apply G_pair; trivial; apply G_trans with omega; trivial; apply zero_omega.
apply G_prodcart; trivial.
Qed.
Lemma G_N : ZFnats.N ∈ U.
pose (f := fun X => singl ZFnats.zero ∪ replf X ZFnats.succ).
assert (fm : morph1 f).
do 2 red; intros.
apply union2_morph; auto with *.
apply replf_morph; trivial.
red; intros; apply ZFnats.succ_morph; trivial.
assert (ZFnats.N ⊆ TI f omega).
red; intros.
apply ZFnats.nat2set_reflect in H.
destruct H.
rewrite H.
clear z H.
induction x; simpl.
apply TI_intro with empty; trivial.
apply union2_intro1.
apply singl_intro.
apply TI_elim in IHx; trivial.
destruct IHx.
apply TI_intro with (osucc x0); auto.
apply union2_intro2.
rewrite replf_ax.
2:do 2 red; intros; apply ZFnats.succ_morph; trivial.
exists (ZFnats.nat2set x); auto with *.
apply TI_intro with x0; auto.
eauto using isOrd_inv.
apply lt_osucc; eauto using isOrd_inv.
apply G_incl with (2:=H); trivial.
apply G_TI; trivial; intros.
apply G_union2; trivial.
apply G_singl; trivial.
apply G_replf; trivial.
do 2 red; intros; apply ZFnats.succ_morph; trivial.
intros.
unfold ZFnats.succ.
apply G_union2; eauto using G_trans.
apply G_singl; trivial.
apply G_trans with x; trivial.
Qed.
Lemma G_osup I f :
ext_fun I f ->
(∀ x, x ∈ I -> isOrd (f x)) ->
I ∈ U ->
(∀ x, x ∈ I -> f x ∈ U) ->
osup I f ∈ U.
intros ef ford IU fU.
apply osup_univ; trivial; intros.
apply G_sup; trivial.
apply G_singl.
apply G_osup2; eauto using G_trans.
apply G_N.
Qed.
Lemma G_Ffix_ord F A :
Proper (incl_set ==> incl_set) F ->
(∀ X, X ⊆ A -> F X ⊆ A) ->
A ∈ U ->
Ffix_ord F A ∈ U.
intros.
unfold Ffix_ord.
apply G_osup; intros; trivial.
do 2 red; intros; apply osucc_morph.
unfold Fix_rec.
apply uchoice_morph_raw.
red; intros.
apply Ffix_rel_morph; trivial.
apply isOrd_succ.
apply F_a_ord; auto.
apply G_Ffix; trivial.
unfold osucc; apply G_subset; trivial; apply G_power; trivial.
apply subset_elim1 with (P:=isOrd).
apply Fix_rec_typ; auto; intros.
apply F_a_morph; trivial.
unfold F_a.
apply subset_intro.
apply G_osup.
do 2 red; intros.
apply osucc_morph; apply H3; trivial.
intros.
apply isOrd_succ.
apply H5 in H6.
apply subset_elim2 in H6; destruct H6.
rewrite H6; trivial.
unfold fsub.
apply G_subset; trivial.
apply G_Ffix; trivial.
intros.
unfold osucc.
apply G_subset; trivial.
apply G_power; trivial.
apply H5 in H6.
apply subset_elim1 in H6; trivial.
apply isOrd_osup.
do 2 red; intros; apply osucc_morph; apply H3; trivial.
intros.
apply isOrd_succ.
apply H5 in H6.
apply subset_elim2 in H6; destruct H6.
rewrite H6; trivial.
Qed.
End Infinite.
End GrothendieckUniverse.
Lemma grot_inter : ∀ UU,
(exists x, x ∈ UU) ->
(∀ x, x ∈ UU -> grot_univ x) ->
grot_univ (inter UU).
destruct 1.
split; intros.
apply inter_intro; intros; eauto.
destruct (H0 _ H3) as (trans,_,_,_).
apply trans with x0; trivial.
apply inter_elim with (1:=H2); trivial.
apply inter_intro; intros; eauto.
destruct (H0 _ H3) as (_,clos_pair,_,_).
apply clos_pair; eapply inter_elim; eauto.
apply inter_intro; intros; eauto.
destruct (H0 _ H2) as (_,_,clos_pow,_).
apply clos_pow; eapply inter_elim; eauto.
apply inter_intro; intros; eauto.
destruct (H0 _ H4) as (_,_,_,clos_union).
apply clos_union; trivial; intros; eapply inter_elim; eauto.
Qed.
Lemma grot_intersection : ∀ (P:set->Prop) x,
grot_univ x -> P x ->
grot_univ (subset x (fun y => ∀ U, grot_univ U -> P U -> y ∈ U)).
intros.
split; intros.
apply subset_intro; intros.
apply G_trans with x0; trivial.
apply subset_elim1 with (1:=H2).
elim subset_elim2 with (1:=H2); intros.
apply G_trans with x0; auto.
rewrite H5; auto.
apply subset_intro; intros.
apply G_pair; trivial.
apply subset_elim1 with (1:=H1).
apply subset_elim1 with (1:=H2).
elim subset_elim2 with (1:=H1); intros.
elim subset_elim2 with (1:=H2); intros.
rewrite H5; rewrite H7.
apply G_pair; auto.
apply subset_intro; intros.
apply G_power; trivial.
apply subset_elim1 with (1:=H1).
elim subset_elim2 with (1:=H1); intros.
rewrite H4.
apply G_power; auto.
apply subset_intro; intros.
apply G_union_repl; intros; trivial.
apply subset_elim1 with (1:=H2).
apply subset_elim1 with (1:=H3 _ _ H4 H5).
apply G_union_repl; intros; auto.
elim subset_elim2 with (1:=H2); intros.
rewrite H6; auto.
elim subset_elim2 with (1:=H3 _ _ H6 H7); intros.
rewrite H8; auto.
Qed.
Definition grot_succ_pred x y :=
grot_univ y /\ x ∈ y /\ ∀ U, grot_univ U -> x ∈ U -> y ⊆ U.
Definition grothendieck := ∀ x, exists2 U, grot_univ U & x ∈ U.
Section TarskiGrothendieck.
Variable gr : grothendieck.
Lemma grot_inter_unique : ∀ x, uchoice_pred (grot_succ_pred x).
unfold grot_succ_pred.
split; intros.
destruct H0 as (H0,(H1,H2)).
split.
apply grot_univ_ext with x0; trivial.
split; intros.
rewrite <- H; trivial.
rewrite <- H; auto.
split; intros.
elim gr with x; intros.
exists (subset x0 (fun y =>
∀ U, grot_univ U -> x ∈ U -> y ∈ U)).
split; intros.
apply (grot_intersection (fun U => x ∈ U) x0); trivial.
split; intros.
apply subset_intro; trivial.
red; intros.
elim subset_elim2 with (1:=H3); intros.
rewrite H4; auto.
destruct H as (gr_x0,(in_x0,lst_x0)).
destruct H0 as (gr_x',(in_x',lst_x')).
red in lst_x0, lst_x'|-.
apply eq_intro; eauto.
Qed.
Definition grot_succ U := uchoice (grot_succ_pred U).
Lemma grot_succ_typ : ∀ x, grot_univ (grot_succ x).
intros.
destruct (uchoice_def (grot_succ_pred x)).
exact (grot_inter_unique x).
trivial.
Qed.
Lemma grot_succ_in : ∀ x, x ∈ grot_succ x.
intros.
destruct (uchoice_def (grot_succ_pred x)).
exact (grot_inter_unique x).
destruct H0; trivial.
Qed.
End TarskiGrothendieck.
Require Import ZFpairs ZFsum ZFrelations ZFrepl ZFwf ZFord ZFfix.
Require Import ZFstable.
Require Import ZFlist.
Record grot_univ (U:set) : Prop := {
G_trans : ∀ x y, y ∈ x -> x ∈ U -> y ∈ U;
G_pair : ∀ x y, x ∈ U -> y ∈ U -> pair x y ∈ U;
G_power : ∀ x, x ∈ U -> power x ∈ U;
G_union_repl : ∀ I R, repl_rel I R -> I ∈ U ->
(∀ x y, x ∈ I -> R x y -> y ∈ U) ->
union (repl I R) ∈ U }.
Lemma grot_univ_ext : ∀ U U',
U == U' -> grot_univ U -> grot_univ U'.
destruct 2; split; intros.
rewrite <- H in H1|-*; eauto.
rewrite <- H in H0,H1|-*; auto.
rewrite <- H in H0|-*; auto.
rewrite <- H in H1|-*.
apply G_union_repl0; intros; auto.
rewrite H; eauto.
Qed.
Lemma grot_empty : grot_univ empty.
split; intros.
elim empty_ax with (1:=H0).
elim empty_ax with (1:=H0).
elim empty_ax with (1:=H).
elim empty_ax with (1:=H0).
Qed.
Section GrothendieckUniverse.
Variable U : set.
Hypothesis grot : grot_univ U.
Lemma G_incl : ∀ x y, x ∈ U -> y ⊆ x -> y ∈ U.
intros.
apply G_trans with (power x); trivial.
rewrite power_ax; auto.
apply G_power; trivial.
Qed.
Lemma G_subset : ∀ x P, x ∈ U -> subset x P ∈ U.
intros.
apply G_incl with x; trivial.
red; intros.
apply subset_elim1 in H0; trivial.
Qed.
Lemma G_singl : ∀ x, x ∈ U -> singl x ∈ U.
unfold singl; intros; apply G_pair; auto.
Qed.
Lemma G_repl : ∀ A R,
repl_rel A R ->
A ∈ U ->
(∀ x y, x ∈ A -> R x y -> y ∈ U) ->
repl A R ∈ U.
intros.
assert (repl_rel A (fun x y => exists2 z, R x z & y == singl z)).
destruct H as (Rext,Rfun).
split; intros.
destruct H4.
exists x0.
apply Rext with x x0; auto; try reflexivity.
transitivity y; auto; symmetry; auto.
destruct H2; destruct H3.
rewrite H4; rewrite H5.
apply singl_morph.
eauto.
setoid_replace (repl A R) with
(union (repl A (fun x y => exists2 z, R x z & y == singl z))).
apply G_union_repl; trivial.
destruct 2.
rewrite H5.
apply G_singl; eauto.
apply union_ext; intros.
elim repl_elim with (2:=H4); trivial; intros.
destruct H6.
rewrite H7 in H3.
rewrite (singl_elim _ _ H3).
apply repl_intro with x0; trivial.
elim repl_elim with (2:=H3); trivial; intros.
exists (singl x).
apply singl_intro.
apply repl_intro with x0; trivial.
exists x; trivial; reflexivity.
Qed.
Lemma G_union : ∀ x, x ∈ U -> union x ∈ U.
intros.
setoid_replace x with (repl x (fun y z => z==y)).
apply G_union_repl; trivial; intros.
apply repl_rel_fun with (f:=fun x:set=>x).
do 2 red; auto.
rewrite H1; apply G_trans with x; trivial.
apply repl_ext; intros.
apply repl_rel_fun with (f:=fun x:set=>x).
do 2 red; auto.
rewrite H1; trivial.
exists y; trivial; reflexivity.
Qed.
Lemma G_replf : ∀ A F,
ext_fun A F ->
A ∈ U ->
(∀ x, x ∈ A -> F x ∈ U) ->
replf A F ∈ U.
unfold replf; intros; apply G_repl; intros; auto.
apply repl_rel_fun; trivial.
rewrite H3; auto.
Qed.
Lemma G_union2 : ∀ x y, x ∈ U -> y ∈ U -> x ∪ y ∈ U.
intros.
unfold union2.
apply G_union.
apply G_pair; trivial.
Qed.
Lemma G_sup A B :
ext_fun A B ->
A ∈ U ->
(∀ x, x ∈ A -> B x ∈ U) ->
sup A B ∈ U.
intros.
apply G_union; trivial.
apply G_replf; trivial.
Qed.
Lemma G_nat x : x ∈ U -> ZFnats.N ⊆ U.
red; intros.
elim H0 using ZFnats.N_ind; intros.
rewrite <- H2; trivial.
apply G_incl with x; trivial.
red; intros.
apply empty_ax in H1; contradiction.
apply G_union2; trivial.
apply G_singl; trivial.
Qed.
Lemma G_prodcart : ∀ A B, A ∈ U -> B ∈ U -> prodcart A B ∈ U.
intros.
unfold prodcart.
apply G_subset; intros; trivial.
apply G_power; trivial.
apply G_power; trivial.
apply G_union2; trivial.
Qed.
Lemma G_couple : ∀ x y, x ∈ U -> y ∈ U -> couple x y ∈ U.
intros.
unfold couple.
apply G_pair; trivial.
apply G_singl; trivial.
apply G_pair; trivial.
Qed.
Lemma G_sum X Y : X ∈ U -> Y ∈ U -> sum X Y ∈ U.
unfold sum; intros.
apply G_union2; apply G_prodcart; trivial.
apply G_singl; apply G_nat with X; trivial.
apply ZFnats.zero_typ.
apply G_singl; apply G_nat with X; trivial.
apply ZFnats.succ_typ; apply ZFnats.zero_typ.
Qed.
Lemma G_sumcase A B f g a :
morph1 f ->
morph1 g ->
a ∈ sum A B ->
(∀ a, a ∈ A -> f a ∈ U) ->
(∀ a, a ∈ B -> g a ∈ U) ->
sum_case f g a ∈ U.
intros.
apply sum_case_ind with (6:=H1); intros; auto.
apply morph_impl_iff1; auto with *.
do 3 red; intros.
rewrite <- H4; trivial.
Qed.
Lemma G_rel : ∀ A B, A ∈ U -> B ∈ U -> rel A B ∈ U.
intros.
unfold rel.
apply G_power; trivial.
apply G_prodcart; trivial.
Qed.
Lemma G_func : ∀ A B, A ∈ U -> B ∈ U -> func A B ∈ U.
intros.
unfold func.
apply G_subset; intros; trivial.
apply G_rel; trivial.
Qed.
Lemma G_dep_func : ∀ X Y,
ext_fun X Y ->
X ∈ U ->
(∀ x, x ∈ X -> Y x ∈ U) ->
dep_func X Y ∈ U.
intros.
unfold dep_func.
apply G_subset; intros; trivial.
apply G_func; trivial.
unfold dep_image.
apply G_union; trivial.
apply G_replf; trivial.
Qed.
Lemma G_app f x :
f ∈ U -> x ∈ U -> app f x ∈ U.
unfold app; intros.
apply G_union.
apply G_subset.
unfold rel_image.
apply G_subset.
apply G_union; trivial.
apply G_union; trivial.
Qed.
Lemma G_sigma A B :
ext_fun A B ->
A ∈ U ->
(∀ x, x ∈ A -> B x ∈ U) ->
sigma A B ∈ U.
intros.
apply G_subset; trivial.
apply G_prodcart; trivial.
apply G_sup; trivial.
Qed.
Lemma G_cc_lam A F :
ext_fun A F ->
A ∈ U ->
(∀ x, x ∈ A -> F x ∈ U) ->
cc_lam A F ∈ U.
intros.
unfold cc_lam.
apply G_sup; intros; trivial.
do 2 red; intros; apply replf_morph; auto.
red; intros; apply couple_morph; trivial.
apply G_replf; intros; auto.
do 2 red; intros; apply couple_morph; auto with *.
apply G_couple; trivial.
apply G_trans with A; trivial.
apply G_trans with (F x); auto.
Qed.
Lemma G_cc_app f x :
f ∈ U -> x ∈ U -> cc_app f x ∈ U.
unfold cc_app; intros.
unfold rel_image.
apply G_subset.
apply G_union.
apply G_union.
apply G_subset; trivial.
Qed.
Lemma G_cc_prod A B :
ext_fun A B ->
A ∈ U ->
(∀ x, x ∈ A -> B x ∈ U) ->
cc_prod A B ∈ U.
intros.
unfold cc_prod.
apply G_replf; auto with *.
apply G_dep_func; intros; auto with *.
intros.
apply G_cc_lam; intros; auto.
do 2 red; intros; apply app_morph; auto with *.
apply G_app.
apply G_trans with (dep_func A B); trivial.
apply G_dep_func; trivial.
apply G_trans with A; trivial.
Qed.
Lemma G_TR F o :
Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F ->
(∀ o f f', isOrd o -> eq_fun o f f' -> F f o == F f' o) ->
isOrd o ->
o ∈ U ->
(∀ f o, ext_fun o f -> o ∈ U ->
(∀ o', o' ∈ o -> f o' ∈ U) ->
F f o ∈ U) ->
TR F o ∈ U.
intros Fm Fext oo oU FU.
apply TR_typ with (X:=fun _ => U); auto.
do 2 red; reflexivity.
intros.
apply FU; auto.
apply G_incl with o; trivial.
Qed.
Lemma G_TI F o :
morph1 F ->
isOrd o ->
o ∈ U ->
(∀ x, x ∈ U -> F x ∈ U) ->
TI F o ∈ U.
intros.
apply G_TR; trivial; intros.
do 3 red; intros.
apply sup_morph; auto.
red; intros; auto.
apply sup_morph; auto with *.
red; intros.
apply H; auto.
apply G_sup; auto.
do 2 red; intros; apply H; auto.
Qed.
Lemma G_osup2 x y :
isWf x -> x ∈ U -> y ∈ U -> x ⊔ y ∈ U.
intro wfx; revert y; induction wfx using isWf_ind.
intros.
rewrite osup2_def; trivial.
apply G_union2; trivial.
apply G_union2; trivial.
apply G_union; trivial.
apply G_replf; trivial; intros.
do 2 red; intros; apply replf_morph; auto with *.
red; intros; apply osup2_morph; trivial.
apply G_replf; trivial; intros.
do 2 red; intros; apply osup2_morph; auto with *.
apply H; eauto using G_trans.
Qed.
Lemma G_Ffix F A : A ∈ U -> Ffix F A ∈ U.
intros.
unfold Ffix.
apply G_subset; trivial.
Qed.
Section NonTrivial.
Hypothesis Unontriv : empty ∈ U.
End NonTrivial.
Section Infinite.
Hypothesis Uinf : omega ∈ U.
Lemma G_inf_nontriv : empty ∈ U.
apply G_trans with omega; trivial.
apply zero_omega.
Qed.
Hint Resolve G_inf_nontriv.
Lemma G_List A : A ∈ U -> List A ∈ U.
intros.
unfold List.
apply G_TI; intros; trivial.
apply LISTf_morph.
unfold LISTf.
apply G_union2; trivial.
apply G_pair; trivial; apply G_trans with omega; trivial; apply zero_omega.
apply G_prodcart; trivial.
Qed.
Lemma G_N : ZFnats.N ∈ U.
pose (f := fun X => singl ZFnats.zero ∪ replf X ZFnats.succ).
assert (fm : morph1 f).
do 2 red; intros.
apply union2_morph; auto with *.
apply replf_morph; trivial.
red; intros; apply ZFnats.succ_morph; trivial.
assert (ZFnats.N ⊆ TI f omega).
red; intros.
apply ZFnats.nat2set_reflect in H.
destruct H.
rewrite H.
clear z H.
induction x; simpl.
apply TI_intro with empty; trivial.
apply union2_intro1.
apply singl_intro.
apply TI_elim in IHx; trivial.
destruct IHx.
apply TI_intro with (osucc x0); auto.
apply union2_intro2.
rewrite replf_ax.
2:do 2 red; intros; apply ZFnats.succ_morph; trivial.
exists (ZFnats.nat2set x); auto with *.
apply TI_intro with x0; auto.
eauto using isOrd_inv.
apply lt_osucc; eauto using isOrd_inv.
apply G_incl with (2:=H); trivial.
apply G_TI; trivial; intros.
apply G_union2; trivial.
apply G_singl; trivial.
apply G_replf; trivial.
do 2 red; intros; apply ZFnats.succ_morph; trivial.
intros.
unfold ZFnats.succ.
apply G_union2; eauto using G_trans.
apply G_singl; trivial.
apply G_trans with x; trivial.
Qed.
Lemma G_osup I f :
ext_fun I f ->
(∀ x, x ∈ I -> isOrd (f x)) ->
I ∈ U ->
(∀ x, x ∈ I -> f x ∈ U) ->
osup I f ∈ U.
intros ef ford IU fU.
apply osup_univ; trivial; intros.
apply G_sup; trivial.
apply G_singl.
apply G_osup2; eauto using G_trans.
apply G_N.
Qed.
Lemma G_Ffix_ord F A :
Proper (incl_set ==> incl_set) F ->
(∀ X, X ⊆ A -> F X ⊆ A) ->
A ∈ U ->
Ffix_ord F A ∈ U.
intros.
unfold Ffix_ord.
apply G_osup; intros; trivial.
do 2 red; intros; apply osucc_morph.
unfold Fix_rec.
apply uchoice_morph_raw.
red; intros.
apply Ffix_rel_morph; trivial.
apply isOrd_succ.
apply F_a_ord; auto.
apply G_Ffix; trivial.
unfold osucc; apply G_subset; trivial; apply G_power; trivial.
apply subset_elim1 with (P:=isOrd).
apply Fix_rec_typ; auto; intros.
apply F_a_morph; trivial.
unfold F_a.
apply subset_intro.
apply G_osup.
do 2 red; intros.
apply osucc_morph; apply H3; trivial.
intros.
apply isOrd_succ.
apply H5 in H6.
apply subset_elim2 in H6; destruct H6.
rewrite H6; trivial.
unfold fsub.
apply G_subset; trivial.
apply G_Ffix; trivial.
intros.
unfold osucc.
apply G_subset; trivial.
apply G_power; trivial.
apply H5 in H6.
apply subset_elim1 in H6; trivial.
apply isOrd_osup.
do 2 red; intros; apply osucc_morph; apply H3; trivial.
intros.
apply isOrd_succ.
apply H5 in H6.
apply subset_elim2 in H6; destruct H6.
rewrite H6; trivial.
Qed.
End Infinite.
End GrothendieckUniverse.
Lemma grot_inter : ∀ UU,
(exists x, x ∈ UU) ->
(∀ x, x ∈ UU -> grot_univ x) ->
grot_univ (inter UU).
destruct 1.
split; intros.
apply inter_intro; intros; eauto.
destruct (H0 _ H3) as (trans,_,_,_).
apply trans with x0; trivial.
apply inter_elim with (1:=H2); trivial.
apply inter_intro; intros; eauto.
destruct (H0 _ H3) as (_,clos_pair,_,_).
apply clos_pair; eapply inter_elim; eauto.
apply inter_intro; intros; eauto.
destruct (H0 _ H2) as (_,_,clos_pow,_).
apply clos_pow; eapply inter_elim; eauto.
apply inter_intro; intros; eauto.
destruct (H0 _ H4) as (_,_,_,clos_union).
apply clos_union; trivial; intros; eapply inter_elim; eauto.
Qed.
Lemma grot_intersection : ∀ (P:set->Prop) x,
grot_univ x -> P x ->
grot_univ (subset x (fun y => ∀ U, grot_univ U -> P U -> y ∈ U)).
intros.
split; intros.
apply subset_intro; intros.
apply G_trans with x0; trivial.
apply subset_elim1 with (1:=H2).
elim subset_elim2 with (1:=H2); intros.
apply G_trans with x0; auto.
rewrite H5; auto.
apply subset_intro; intros.
apply G_pair; trivial.
apply subset_elim1 with (1:=H1).
apply subset_elim1 with (1:=H2).
elim subset_elim2 with (1:=H1); intros.
elim subset_elim2 with (1:=H2); intros.
rewrite H5; rewrite H7.
apply G_pair; auto.
apply subset_intro; intros.
apply G_power; trivial.
apply subset_elim1 with (1:=H1).
elim subset_elim2 with (1:=H1); intros.
rewrite H4.
apply G_power; auto.
apply subset_intro; intros.
apply G_union_repl; intros; trivial.
apply subset_elim1 with (1:=H2).
apply subset_elim1 with (1:=H3 _ _ H4 H5).
apply G_union_repl; intros; auto.
elim subset_elim2 with (1:=H2); intros.
rewrite H6; auto.
elim subset_elim2 with (1:=H3 _ _ H6 H7); intros.
rewrite H8; auto.
Qed.
Definition grot_succ_pred x y :=
grot_univ y /\ x ∈ y /\ ∀ U, grot_univ U -> x ∈ U -> y ⊆ U.
Definition grothendieck := ∀ x, exists2 U, grot_univ U & x ∈ U.
Section TarskiGrothendieck.
Variable gr : grothendieck.
Lemma grot_inter_unique : ∀ x, uchoice_pred (grot_succ_pred x).
unfold grot_succ_pred.
split; intros.
destruct H0 as (H0,(H1,H2)).
split.
apply grot_univ_ext with x0; trivial.
split; intros.
rewrite <- H; trivial.
rewrite <- H; auto.
split; intros.
elim gr with x; intros.
exists (subset x0 (fun y =>
∀ U, grot_univ U -> x ∈ U -> y ∈ U)).
split; intros.
apply (grot_intersection (fun U => x ∈ U) x0); trivial.
split; intros.
apply subset_intro; trivial.
red; intros.
elim subset_elim2 with (1:=H3); intros.
rewrite H4; auto.
destruct H as (gr_x0,(in_x0,lst_x0)).
destruct H0 as (gr_x',(in_x',lst_x')).
red in lst_x0, lst_x'|-.
apply eq_intro; eauto.
Qed.
Definition grot_succ U := uchoice (grot_succ_pred U).
Lemma grot_succ_typ : ∀ x, grot_univ (grot_succ x).
intros.
destruct (uchoice_def (grot_succ_pred x)).
exact (grot_inter_unique x).
trivial.
Qed.
Lemma grot_succ_in : ∀ x, x ∈ grot_succ x.
intros.
destruct (uchoice_def (grot_succ_pred x)).
exact (grot_inter_unique x).
destruct H0; trivial.
Qed.
End TarskiGrothendieck.