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.