Let S be given.
Assume HS: countable_set S.
We will prove countable_set (finite_subcollections S).
We will prove countable (finite_subcollections S).
We will prove ∃h : set → set, inj (finite_subcollections S) ω h.
Apply HS to the current goal.
Let f of type set → set be given.
Assume Hf: inj S ω f.
We prove the intermediate claim HFinOmega: countable (finite_subcollections ω).
An exact proof term for the current goal is finite_subcollections_omega_countable.
Apply HFinOmega to the current goal.
Let code of type set → set be given.
Assume Hcode: inj (finite_subcollections ω) ω code.
Set ImgF to be the term λF ⇒ {f x|x ∈ F} of type set → set.
Set h to be the term λF ⇒ code (ImgF F) of type set → set.
We use h to witness the existential quantifier.
Apply (injI (finite_subcollections S) ω h) to the current goal.
Let F be given.
Assume HF: F ∈ finite_subcollections S.
We will prove h F ∈ ω.
We prove the intermediate claim HFpow: F ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim Hfmap: ∀a ∈ S, f a ∈ ω.
An exact proof term for the current goal is (andEL (∀a ∈ S, f a ∈ ω) (∀a b ∈ S, f a = f b → a = b) Hf).
We prove the intermediate claim HImgPow: ImgF F ∈ 𝒫 ω.
An exact proof term for the current goal is (image_In_Power S ω f Hfmap F HFpow).
We prove the intermediate claim HImgFin: finite (ImgF F).
An exact proof term for the current goal is (Repl_finite f F HFfin).
We prove the intermediate claim HImg: ImgF F ∈ finite_subcollections ω.
An exact proof term for the current goal is (SepI (𝒫 ω) (λF0 : set ⇒ finite F0) (ImgF F) HImgPow HImgFin).
We prove the intermediate claim Hcodemap: ∀u ∈ finite_subcollections ω, code u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ finite_subcollections ω, code u ∈ ω) (∀u v ∈ finite_subcollections ω, code u = code v → u = v) Hcode).
We prove the intermediate claim Hhdef: h F = code (ImgF F).
Use reflexivity.
rewrite the current goal using Hhdef (from left to right).
An exact proof term for the current goal is (Hcodemap (ImgF F) HImg).
Let F1 be given.
Assume HF1: F1 ∈ finite_subcollections S.
Let F2 be given.
Assume HF2: F2 ∈ finite_subcollections S.
Assume Heq: h F1 = h F2.
We will prove F1 = F2.
We prove the intermediate claim HF1pow: F1 ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) F1 HF1).
We prove the intermediate claim HF2pow: F2 ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) F2 HF2).
We prove the intermediate claim HF1sub: F1 ⊆ S.
An exact proof term for the current goal is (PowerE S F1 HF1pow).
We prove the intermediate claim HF2sub: F2 ⊆ S.
An exact proof term for the current goal is (PowerE S F2 HF2pow).
We prove the intermediate claim Hf_inj: ∀a b ∈ S, f a = f b → a = b.
An exact proof term for the current goal is (andER (∀a ∈ S, f a ∈ ω) (∀a b ∈ S, f a = f b → a = b) Hf).
We prove the intermediate claim Hfmap: ∀a ∈ S, f a ∈ ω.
An exact proof term for the current goal is (andEL (∀a ∈ S, f a ∈ ω) (∀a b ∈ S, f a = f b → a = b) Hf).
We prove the intermediate claim HImg1: ImgF F1 ∈ finite_subcollections ω.
We prove the intermediate claim HF1fin: finite F1.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) F1 HF1).
We prove the intermediate claim HImgPow: ImgF F1 ∈ 𝒫 ω.
An exact proof term for the current goal is (image_In_Power S ω f Hfmap F1 HF1pow).
We prove the intermediate claim HImgFin: finite (ImgF F1).
An exact proof term for the current goal is (Repl_finite f F1 HF1fin).
An exact proof term for the current goal is (SepI (𝒫 ω) (λF0 : set ⇒ finite F0) (ImgF F1) HImgPow HImgFin).
We prove the intermediate claim HImg2: ImgF F2 ∈ finite_subcollections ω.
We prove the intermediate claim HF2fin: finite F2.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) F2 HF2).
We prove the intermediate claim HImgPow: ImgF F2 ∈ 𝒫 ω.
An exact proof term for the current goal is (image_In_Power S ω f Hfmap F2 HF2pow).
We prove the intermediate claim HImgFin: finite (ImgF F2).
An exact proof term for the current goal is (Repl_finite f F2 HF2fin).
An exact proof term for the current goal is (SepI (𝒫 ω) (λF0 : set ⇒ finite F0) (ImgF F2) HImgPow HImgFin).
We prove the intermediate claim Hcodeinj: ∀u v ∈ finite_subcollections ω, code u = code v → u = v.
An exact proof term for the current goal is (andER (∀u ∈ finite_subcollections ω, code u ∈ ω) (∀u v ∈ finite_subcollections ω, code u = code v → u = v) Hcode).
We prove the intermediate claim Hhdef1: h F1 = code (ImgF F1).
Use reflexivity.
We prove the intermediate claim Hhdef2: h F2 = code (ImgF F2).
Use reflexivity.
We prove the intermediate claim HeqImg: ImgF F1 = ImgF F2.
Apply (Hcodeinj (ImgF F1) HImg1 (ImgF F2) HImg2) to the current goal.
We prove the intermediate claim Hcodeeq: code (ImgF F1) = code (ImgF F2).
We prove the intermediate claim Hc1: code (ImgF F1) = h F1.
Use symmetry.
An exact proof term for the current goal is Hhdef1.
We prove the intermediate claim Hc2: h F2 = code (ImgF F2).
An exact proof term for the current goal is Hhdef2.
We prove the intermediate claim Hmid: code (ImgF F1) = h F2.
An exact proof term for the current goal is (eq_i_tra (code (ImgF F1)) (h F1) (h F2) Hc1 Heq).
An exact proof term for the current goal is (eq_i_tra (code (ImgF F1)) (h F2) (code (ImgF F2)) Hmid Hc2).
An exact proof term for the current goal is Hcodeeq.
Apply set_ext to the current goal.
Let x be given.
Assume Hx1: x ∈ F1.
We will prove x ∈ F2.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (HF1sub x Hx1).
We prove the intermediate claim Hfx1: f x ∈ ImgF F1.
An exact proof term for the current goal is (ReplI F1 f x Hx1).
We prove the intermediate claim Hfx2: f x ∈ ImgF F2.
rewrite the current goal using HeqImg (from right to left).
An exact proof term for the current goal is Hfx1.
Apply (ReplE_impred F2 f (f x) Hfx2) to the current goal.
Let y be given.
Assume Hy2: y ∈ F2.
Assume Hfxy: f x = f y.
We prove the intermediate claim HyS: y ∈ S.
An exact proof term for the current goal is (HF2sub y Hy2).
We prove the intermediate claim Heqxy: x = y.
An exact proof term for the current goal is (Hf_inj x HxS y HyS Hfxy).
rewrite the current goal using Heqxy (from left to right).
An exact proof term for the current goal is Hy2.
Let x be given.
Assume Hx2: x ∈ F2.
We will prove x ∈ F1.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (HF2sub x Hx2).
We prove the intermediate claim Hfx2: f x ∈ ImgF F2.
An exact proof term for the current goal is (ReplI F2 f x Hx2).
We prove the intermediate claim Hfx1: f x ∈ ImgF F1.
rewrite the current goal using HeqImg (from left to right).
An exact proof term for the current goal is Hfx2.
Apply (ReplE_impred F1 f (f x) Hfx1) to the current goal.
Let y be given.
Assume Hy1: y ∈ F1.
Assume Hfxy: f x = f y.
We prove the intermediate claim HyS: y ∈ S.
An exact proof term for the current goal is (HF1sub y Hy1).
We prove the intermediate claim Heqxy: x = y.
An exact proof term for the current goal is (Hf_inj x HxS y HyS Hfxy).
rewrite the current goal using Heqxy (from left to right).
An exact proof term for the current goal is Hy1.
∎