Library ZFecc
Require Import ZF ZFpairs ZFnats ZFgrothendieck.
Require Import ZFrelations ZFcoc.
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 : ∀ n, grot_univ (ecc n).
Lemma ecc_in1 : ∀ n, props ∈ ecc n.
Lemma ecc_in2 : ∀ n, ecc n ∈ ecc (S n).
Lemma ecc_incl : ∀ n x, x ∈ ecc n -> x ∈ ecc (S n).
Lemma ecc_incl_prop : ∀ x, x ∈ props -> x ∈ ecc 0.
Lemma ecc_prod : ∀ n X Y,
ext_fun X Y ->
X ∈ ecc n ->
(∀ x, x ∈ X -> Y x ∈ ecc n) ->
cc_prod X Y ∈ ecc n.
Lemma ecc_prod2 : ∀ n X Y,
ext_fun X Y ->
X ∈ props ->
(∀ x, x ∈ X -> Y x ∈ ecc n) ->
cc_prod X Y ∈ ecc n.
Require Import ZFrelations ZFcoc.
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 : ∀ n, grot_univ (ecc n).
Lemma ecc_in1 : ∀ n, props ∈ ecc n.
Lemma ecc_in2 : ∀ n, ecc n ∈ ecc (S n).
Lemma ecc_incl : ∀ n x, x ∈ ecc n -> x ∈ ecc (S n).
Lemma ecc_incl_prop : ∀ x, x ∈ props -> x ∈ ecc 0.
Lemma ecc_prod : ∀ n X Y,
ext_fun X Y ->
X ∈ ecc n ->
(∀ x, x ∈ X -> Y x ∈ ecc n) ->
cc_prod X Y ∈ ecc n.
Lemma ecc_prod2 : ∀ n X Y,
ext_fun X Y ->
X ∈ props ->
(∀ x, x ∈ X -> Y x ∈ ecc n) ->
cc_prod X Y ∈ ecc n.