Library ZFecc
Require Import ZF ZFpairs ZFnats ZFgrothendieck.
Require Import ZFcoc.
Import IZF.
Axiom gr : grothendieck.
Fixpoint ecc (n:nat) : set :=
match n with
| 0 => grot_succ props
| S k => grot_succ (ecc k)
end.
Lemma ecc_grot : forall n, grot_univ (ecc n).
Lemma ecc_in1 : forall n, props \in ecc n.
Lemma ecc_in2 : forall n, ecc n \in ecc (S n).
Lemma ecc_incl : forall n x, x \in ecc n -> x \in ecc (S n).
Lemma cc_prod_univ : forall X Y U,
grot_univ U ->
ext_fun X Y ->
X \in U ->
(forall x, x \in X -> Y x \in U) ->
cc_prod X Y \in U.
Lemma ecc_prod : forall n X Y,
ext_fun X Y ->
X \in ecc n ->
(forall x, x \in X -> Y x \in ecc n) ->
cc_prod X Y \in ecc n.
Lemma ecc_prod2 : forall n X Y,
ext_fun X Y ->
X \in props ->
(forall x, x \in X -> Y x \in ecc n) ->
cc_prod X Y \in ecc n.
Require Import ZFcoc.
Import IZF.
Axiom gr : grothendieck.
Fixpoint ecc (n:nat) : set :=
match n with
| 0 => grot_succ props
| S k => grot_succ (ecc k)
end.
Lemma ecc_grot : forall n, grot_univ (ecc n).
Lemma ecc_in1 : forall n, props \in ecc n.
Lemma ecc_in2 : forall n, ecc n \in ecc (S n).
Lemma ecc_incl : forall n x, x \in ecc n -> x \in ecc (S n).
Lemma cc_prod_univ : forall X Y U,
grot_univ U ->
ext_fun X Y ->
X \in U ->
(forall x, x \in X -> Y x \in U) ->
cc_prod X Y \in U.
Lemma ecc_prod : forall n X Y,
ext_fun X Y ->
X \in ecc n ->
(forall x, x \in X -> Y x \in ecc n) ->
cc_prod X Y \in ecc n.
Lemma ecc_prod2 : forall n X Y,
ext_fun X Y ->
X \in props ->
(forall x, x \in X -> Y x \in ecc n) ->
cc_prod X Y \in ecc n.