Let X be given.
Assume HX: countable X.
Let Y be given.
Assume HY: ∀x : set, x ∈ X → countable (Y x).
We will prove countable (∑x ∈ X, Y x).
We will prove ∃h : set → set, inj (∑x ∈ X, Y x) ω h.
Apply HX to the current goal.
Let f of type set → set be given.
Assume Hf: inj X ω f.
Set graph to be the term λA g ⇒ {(a,g a)|a ∈ A} of type set → (set → set) → set.
Set app to be the term λg a ⇒ Eps_i (λn ⇒ (a,n) ∈ g) of type set → set → set.
Set G to be the term λx ⇒ Eps_i (λg ⇒ ∃hx : set → set, inj (Y x) ω hx ∧ g = graph (Y x) hx) of type set → set.
Set h to be the term λz ⇒ nat_pair (f (proj0 z)) (app (G (proj0 z)) (proj1 z)) of type set → set.
We use h to witness the existential quantifier.
We prove the intermediate claim graph_app: ∀A : set, ∀g : set → set, ∀a : set, a ∈ A → app (graph A g) a = g a.
Let A, g and a be given.
Assume Ha: a ∈ A.
We will prove app (graph A g) a = g a.
We will prove Eps_i (λn ⇒ (a,n) ∈ graph A g) = g a.
We prove the intermediate claim H1: (a,g a) ∈ graph A g.
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ (a0,g a0)) a Ha).
We prove the intermediate claim H2: (a,Eps_i (λn ⇒ (a,n) ∈ graph A g)) ∈ graph A g.
An exact proof term for the current goal is (Eps_i_ax (λn ⇒ (a,n) ∈ graph A g) (g a) H1).
Apply (ReplE_impred A (λa0 : set ⇒ (a0,g a0)) (a,Eps_i (λn ⇒ (a,n) ∈ graph A g)) H2) to the current goal.
Let a0 be given.
Assume Ha0: a0 ∈ A.
Assume Heq: (a,Eps_i (λn ⇒ (a,n) ∈ graph A g)) = (a0,g a0).
We prove the intermediate claim Ha_eq: a = a0.
rewrite the current goal using (tuple_2_0_eq a (Eps_i (λn ⇒ (a,n) ∈ graph A g))) (from right to left).
rewrite the current goal using (tuple_2_0_eq a0 (g a0)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hn_eq: Eps_i (λn ⇒ (a,n) ∈ graph A g) = g a0.
rewrite the current goal using (tuple_2_1_eq a (Eps_i (λn ⇒ (a,n) ∈ graph A g))) (from right to left) at position 1.
rewrite the current goal using (tuple_2_1_eq a0 (g a0)) (from right to left) at position 1.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
rewrite the current goal using Hn_eq (from left to right).
rewrite the current goal using Ha_eq (from right to left).
Use reflexivity.
We prove the intermediate claim graph_app_eq: ∀A : set, ∀g : set → set, ∀G0 a : set, a ∈ A → G0 = graph A g → app G0 a = g a.
Let A, g, G0 and a be given.
Assume Ha: a ∈ A.
Assume Heq: G0 = graph A g.
We will prove app G0 a = g a.
We will prove Eps_i (λn ⇒ (a,n) ∈ G0) = g a.
We prove the intermediate claim H1: (a,g a) ∈ G0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ (a0,g a0)) a Ha).
We prove the intermediate claim H2: (a,Eps_i (λn ⇒ (a,n) ∈ G0)) ∈ G0.
An exact proof term for the current goal is (Eps_i_ax (λn ⇒ (a,n) ∈ G0) (g a) H1).
We prove the intermediate claim H2g: (a,Eps_i (λn ⇒ (a,n) ∈ G0)) ∈ graph A g.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is H2.
Apply (ReplE_impred A (λa0 : set ⇒ (a0,g a0)) (a,Eps_i (λn ⇒ (a,n) ∈ G0)) H2g) to the current goal.
Let a0 be given.
Assume Ha0: a0 ∈ A.
Assume Heq2: (a,Eps_i (λn ⇒ (a,n) ∈ G0)) = (a0,g a0).
We prove the intermediate claim Ha_eq: a = a0.
rewrite the current goal using (tuple_2_0_eq a (Eps_i (λn ⇒ (a,n) ∈ G0))) (from right to left).
rewrite the current goal using (tuple_2_0_eq a0 (g a0)) (from right to left).
rewrite the current goal using Heq2 (from left to right).
Use reflexivity.
We prove the intermediate claim Hn_eq: Eps_i (λn ⇒ (a,n) ∈ G0) = g a0.
rewrite the current goal using (tuple_2_1_eq a (Eps_i (λn ⇒ (a,n) ∈ G0))) (from right to left) at position 1.
rewrite the current goal using (tuple_2_1_eq a0 (g a0)) (from right to left) at position 1.
rewrite the current goal using Heq2 (from left to right).
Use reflexivity.
rewrite the current goal using Hn_eq (from left to right).
rewrite the current goal using Ha_eq (from right to left).
Use reflexivity.
Apply (injI (∑x ∈ X, Y x) ω h) to the current goal.
Let z be given.
Assume Hz: z ∈ ∑x ∈ X, Y x.
We will prove h z ∈ ω.
We prove the intermediate claim Hz0: proj0 z ∈ X.
An exact proof term for the current goal is (proj0_Sigma X Y z Hz).
We prove the intermediate claim Hz1: proj1 z ∈ Y (proj0 z).
An exact proof term for the current goal is (proj1_Sigma X Y z Hz).
We prove the intermediate claim Hfmap: ∀a ∈ X, f a ∈ ω.
An exact proof term for the current goal is (andEL (∀a ∈ X, f a ∈ ω) (∀a b ∈ X, f a = f b → a = b) Hf).
We prove the intermediate claim Hfz: f (proj0 z) ∈ ω.
An exact proof term for the current goal is (Hfmap (proj0 z) Hz0).
Set x0 to be the term proj0 z.
We prove the intermediate claim HcountY: countable (Y x0).
An exact proof term for the current goal is (HY x0 Hz0).
Apply HcountY to the current goal.
Let hx of type set → set be given.
Assume Hhx: inj (Y x0) ω hx.
We prove the intermediate claim HPw: ∃hx0 : set → set, inj (Y x0) ω hx0 ∧ graph (Y x0) hx = graph (Y x0) hx0.
We use hx to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hhx.
Use reflexivity.
We prove the intermediate claim HGdef: G x0 = Eps_i (λg ⇒ ∃hx0 : set → set, inj (Y x0) ω hx0 ∧ g = graph (Y x0) hx0).
Use reflexivity.
We prove the intermediate claim HQG: ∃hx0 : set → set, inj (Y x0) ω hx0 ∧ G x0 = graph (Y x0) hx0.
rewrite the current goal using HGdef (from left to right).
An exact proof term for the current goal is (Eps_i_ax (λg ⇒ ∃hx0 : set → set, inj (Y x0) ω hx0 ∧ g = graph (Y x0) hx0) (graph (Y x0) hx) HPw).
Apply HQG to the current goal.
Let hx0 of type set → set be given.
Assume Hhx0pair.
Apply Hhx0pair to the current goal.
Assume Hhx0 HGeq.
We prove the intermediate claim Hhx0map: ∀u ∈ Y x0, hx0 u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Y x0, hx0 u ∈ ω) (∀u v ∈ Y x0, hx0 u = hx0 v → u = v) Hhx0).
We prove the intermediate claim Hhy: hx0 (proj1 z) ∈ ω.
An exact proof term for the current goal is (Hhx0map (proj1 z) Hz1).
We prove the intermediate claim Happ: app (G x0) (proj1 z) = hx0 (proj1 z).
An exact proof term for the current goal is (graph_app_eq (Y x0) hx0 (G x0) (proj1 z) Hz1 HGeq).
We prove the intermediate claim Hhdef: h z = nat_pair (f (proj0 z)) (app (G (proj0 z)) (proj1 z)).
Use reflexivity.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (nat_pair_In_omega (f (proj0 z)) Hfz (hx0 (proj1 z)) Hhy).
Let z1 be given.
Assume Hz1: z1 ∈ ∑x ∈ X, Y x.
Let z2 be given.
Assume Hz2: z2 ∈ ∑x ∈ X, Y x.
Assume Heq: h z1 = h z2.
We will prove z1 = z2.
We prove the intermediate claim Hz10: proj0 z1 ∈ X.
An exact proof term for the current goal is (proj0_Sigma X Y z1 Hz1).
We prove the intermediate claim Hz20: proj0 z2 ∈ X.
An exact proof term for the current goal is (proj0_Sigma X Y z2 Hz2).
We prove the intermediate claim Hz11: proj1 z1 ∈ Y (proj0 z1).
An exact proof term for the current goal is (proj1_Sigma X Y z1 Hz1).
We prove the intermediate claim Hz21: proj1 z2 ∈ Y (proj0 z2).
An exact proof term for the current goal is (proj1_Sigma X Y z2 Hz2).
We prove the intermediate claim Hfmap: ∀a ∈ X, f a ∈ ω.
An exact proof term for the current goal is (andEL (∀a ∈ X, f a ∈ ω) (∀a b ∈ X, f a = f b → a = b) Hf).
We prove the intermediate claim Hfinj: ∀a b ∈ X, f a = f b → a = b.
An exact proof term for the current goal is (andER (∀a ∈ X, f a ∈ ω) (∀a b ∈ X, f a = f b → a = b) Hf).
We prove the intermediate claim Hfz1: f (proj0 z1) ∈ ω.
An exact proof term for the current goal is (Hfmap (proj0 z1) Hz10).
We prove the intermediate claim Hfz2: f (proj0 z2) ∈ ω.
An exact proof term for the current goal is (Hfmap (proj0 z2) Hz20).
We prove the intermediate claim Hhy1: app (G (proj0 z1)) (proj1 z1) ∈ ω.
Set x1 to be the term proj0 z1.
We prove the intermediate claim HcountY: countable (Y x1).
An exact proof term for the current goal is (HY x1 Hz10).
Apply HcountY to the current goal.
Let hx of type set → set be given.
Assume Hhx: inj (Y x1) ω hx.
We prove the intermediate claim HPw: ∃hx0 : set → set, inj (Y x1) ω hx0 ∧ graph (Y x1) hx = graph (Y x1) hx0.
We use hx to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hhx.
Use reflexivity.
We prove the intermediate claim HGdef: G x1 = Eps_i (λg ⇒ ∃hx0 : set → set, inj (Y x1) ω hx0 ∧ g = graph (Y x1) hx0).
Use reflexivity.
We prove the intermediate claim HQG: ∃hx0 : set → set, inj (Y x1) ω hx0 ∧ G x1 = graph (Y x1) hx0.
rewrite the current goal using HGdef (from left to right).
An exact proof term for the current goal is (Eps_i_ax (λg ⇒ ∃hx0 : set → set, inj (Y x1) ω hx0 ∧ g = graph (Y x1) hx0) (graph (Y x1) hx) HPw).
Apply HQG to the current goal.
Let hx0 of type set → set be given.
Assume Hhx0pair.
Apply Hhx0pair to the current goal.
Assume Hhx0 HGeq.
We prove the intermediate claim Hhx0map: ∀u ∈ Y x1, hx0 u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Y x1, hx0 u ∈ ω) (∀u v ∈ Y x1, hx0 u = hx0 v → u = v) Hhx0).
We prove the intermediate claim Hhy: hx0 (proj1 z1) ∈ ω.
An exact proof term for the current goal is (Hhx0map (proj1 z1) Hz11).
We prove the intermediate claim Happ: app (G x1) (proj1 z1) = hx0 (proj1 z1).
An exact proof term for the current goal is (graph_app_eq (Y x1) hx0 (G x1) (proj1 z1) Hz11 HGeq).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is Hhy.
We prove the intermediate claim Hhy2: app (G (proj0 z2)) (proj1 z2) ∈ ω.
Set x2 to be the term proj0 z2.
We prove the intermediate claim HcountY: countable (Y x2).
An exact proof term for the current goal is (HY x2 Hz20).
Apply HcountY to the current goal.
Let hx of type set → set be given.
Assume Hhx: inj (Y x2) ω hx.
We prove the intermediate claim HPw: ∃hx0 : set → set, inj (Y x2) ω hx0 ∧ graph (Y x2) hx = graph (Y x2) hx0.
We use hx to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hhx.
Use reflexivity.
We prove the intermediate claim HGdef: G x2 = Eps_i (λg ⇒ ∃hx0 : set → set, inj (Y x2) ω hx0 ∧ g = graph (Y x2) hx0).
Use reflexivity.
We prove the intermediate claim HQG: ∃hx0 : set → set, inj (Y x2) ω hx0 ∧ G x2 = graph (Y x2) hx0.
rewrite the current goal using HGdef (from left to right).
An exact proof term for the current goal is (Eps_i_ax (λg ⇒ ∃hx0 : set → set, inj (Y x2) ω hx0 ∧ g = graph (Y x2) hx0) (graph (Y x2) hx) HPw).
Apply HQG to the current goal.
Let hx0 of type set → set be given.
Assume Hhx0pair.
Apply Hhx0pair to the current goal.
Assume Hhx0 HGeq.
We prove the intermediate claim Hhx0map: ∀u ∈ Y x2, hx0 u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Y x2, hx0 u ∈ ω) (∀u v ∈ Y x2, hx0 u = hx0 v → u = v) Hhx0).
We prove the intermediate claim Hhy: hx0 (proj1 z2) ∈ ω.
An exact proof term for the current goal is (Hhx0map (proj1 z2) Hz21).
We prove the intermediate claim Happ: app (G x2) (proj1 z2) = hx0 (proj1 z2).
An exact proof term for the current goal is (graph_app_eq (Y x2) hx0 (G x2) (proj1 z2) Hz21 HGeq).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is Hhy.
We prove the intermediate claim Hhdef1: h z1 = nat_pair (f (proj0 z1)) (app (G (proj0 z1)) (proj1 z1)).
Use reflexivity.
We prove the intermediate claim Hhdef2: h z2 = nat_pair (f (proj0 z2)) (app (G (proj0 z2)) (proj1 z2)).
Use reflexivity.
We prove the intermediate claim Hpair: nat_pair (f (proj0 z1)) (app (G (proj0 z1)) (proj1 z1)) = nat_pair (f (proj0 z2)) (app (G (proj0 z2)) (proj1 z2)).
rewrite the current goal using Hhdef1 (from right to left).
rewrite the current goal using Hhdef2 (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim Hxeq: proj0 z1 = proj0 z2.
We prove the intermediate claim Hf0: f (proj0 z1) = f (proj0 z2).
An exact proof term for the current goal is (nat_pair_0 (f (proj0 z1)) Hfz1 (app (G (proj0 z1)) (proj1 z1)) Hhy1 (f (proj0 z2)) Hfz2 (app (G (proj0 z2)) (proj1 z2)) Hhy2 Hpair).
An exact proof term for the current goal is (Hfinj (proj0 z1) Hz10 (proj0 z2) Hz20 Hf0).
Set x to be the term proj0 z1.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is Hz10.
We prove the intermediate claim Hz2x: proj0 z2 = x.
Use symmetry.
An exact proof term for the current goal is Hxeq.
We prove the intermediate claim Hy21': proj1 z2 ∈ Y x.
rewrite the current goal using Hz2x (from right to left).
An exact proof term for the current goal is Hz21.
We prove the intermediate claim Hy11': proj1 z1 ∈ Y x.
We prove the intermediate claim Hxdef: x = proj0 z1.
Use reflexivity.
rewrite the current goal using Hxdef (from left to right).
An exact proof term for the current goal is Hz11.
We prove the intermediate claim HcountY: countable (Y x).
An exact proof term for the current goal is (HY x HxX).
Apply HcountY to the current goal.
Let hx of type set → set be given.
Assume Hhx: inj (Y x) ω hx.
We prove the intermediate claim HPw: ∃hx0 : set → set, inj (Y x) ω hx0 ∧ graph (Y x) hx = graph (Y x) hx0.
We use hx to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hhx.
Use reflexivity.
We prove the intermediate claim HGdef: G x = Eps_i (λg ⇒ ∃hx0 : set → set, inj (Y x) ω hx0 ∧ g = graph (Y x) hx0).
Use reflexivity.
We prove the intermediate claim HQG: ∃hx0 : set → set, inj (Y x) ω hx0 ∧ G x = graph (Y x) hx0.
rewrite the current goal using HGdef (from left to right).
An exact proof term for the current goal is (Eps_i_ax (λg ⇒ ∃hx0 : set → set, inj (Y x) ω hx0 ∧ g = graph (Y x) hx0) (graph (Y x) hx) HPw).
Apply HQG to the current goal.
Let hx0 of type set → set be given.
Assume Hhx0pair.
Apply Hhx0pair to the current goal.
Assume Hhx0 HGeq.
We prove the intermediate claim Hhx0inj: ∀u v ∈ Y x, hx0 u = hx0 v → u = v.
An exact proof term for the current goal is (andER (∀u ∈ Y x, hx0 u ∈ ω) (∀u v ∈ Y x, hx0 u = hx0 v → u = v) Hhx0).
We prove the intermediate claim Happ1: app (G x) (proj1 z1) = hx0 (proj1 z1).
An exact proof term for the current goal is (graph_app_eq (Y x) hx0 (G x) (proj1 z1) Hy11' HGeq).
We prove the intermediate claim Happ2: app (G x) (proj1 z2) = hx0 (proj1 z2).
An exact proof term for the current goal is (graph_app_eq (Y x) hx0 (G x) (proj1 z2) Hy21' HGeq).
We prove the intermediate claim Hn_eq: app (G x) (proj1 z1) = app (G x) (proj1 z2).
We prove the intermediate claim Hn0: app (G (proj0 z1)) (proj1 z1) = app (G (proj0 z2)) (proj1 z2).
An exact proof term for the current goal is (nat_pair_1 (f (proj0 z1)) Hfz1 (app (G (proj0 z1)) (proj1 z1)) Hhy1 (f (proj0 z2)) Hfz2 (app (G (proj0 z2)) (proj1 z2)) Hhy2 Hpair).
We prove the intermediate claim Hxdef: x = proj0 z1.
Use reflexivity.
rewrite the current goal using Hxdef (from left to right).
rewrite the current goal using Hxeq (from left to right) at position 2.
An exact proof term for the current goal is Hn0.
We prove the intermediate claim Hhx0eq: hx0 (proj1 z1) = hx0 (proj1 z2).
rewrite the current goal using Happ1 (from right to left).
rewrite the current goal using Happ2 (from right to left).
An exact proof term for the current goal is Hn_eq.
We prove the intermediate claim Hyeq: proj1 z1 = proj1 z2.
An exact proof term for the current goal is (Hhx0inj (proj1 z1) Hy11' (proj1 z2) Hy21' Hhx0eq).
Apply (Sigma_eta_proj0_proj1 X Y z1 Hz1) to the current goal.
Assume Heta1core Heta1Y.
Apply Heta1core to the current goal.
Assume Heta1 Heta1X.
Apply (Sigma_eta_proj0_proj1 X Y z2 Hz2) to the current goal.
Assume Heta2core Heta2Y.
Apply Heta2core to the current goal.
Assume Heta2 Heta2X.
rewrite the current goal using Heta1 (from right to left).
rewrite the current goal using Heta2 (from right to left).
rewrite the current goal using Hxeq (from left to right).
rewrite the current goal using Hyeq (from left to right).
Use reflexivity.
∎