Let X be given.
Assume HX: countable_set X.
Let F be given.
We will prove countable_set {F x|x ∈ X}.
We will prove countable {F x|x ∈ X}.
We will prove atleastp {F x|x ∈ X} ω.
We will prove ∃g : set → set, inj {F x|x ∈ X} ω g.
Apply HX to the current goal.
Let h of type set → set be given.
Assume Hh: inj X ω h.
Set pre to be the term λy ⇒ Eps_i (λx ⇒ x ∈ X ∧ y = F x) of type set → set.
Set g to be the term λy ⇒ h (pre y) of type set → set.
We use g to witness the existential quantifier.
Apply (injI {F x|x ∈ X} ω g) to the current goal.
Let y be given.
Assume Hy: y ∈ {F x|x ∈ X}.
We will prove g y ∈ ω.
Apply (ReplE_impred X F y Hy) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
Assume HyFx: y = F x.
We prove the intermediate claim Hpreprop: pre y ∈ X ∧ y = F (pre y).
An exact proof term for the current goal is (Eps_i_ax (λx0 ⇒ x0 ∈ X ∧ y = F x0) x (andI (x ∈ X) (y = F x) HxX HyFx)).
We prove the intermediate claim HpreX: pre y ∈ X.
An exact proof term for the current goal is (andEL (pre y ∈ X) (y = F (pre y)) Hpreprop).
We prove the intermediate claim Hhmap: ∀u ∈ X, h u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ X, h u ∈ ω) (∀u v ∈ X, h u = h v → u = v) Hh).
We prove the intermediate claim Hgy: g y = h (pre y).
Use reflexivity.
rewrite the current goal using Hgy (from left to right).
An exact proof term for the current goal is (Hhmap (pre y) HpreX).
Let y1 be given.
Assume Hy1: y1 ∈ {F x|x ∈ X}.
Let y2 be given.
Assume Hy2: y2 ∈ {F x|x ∈ X}.
Assume Hg: g y1 = g y2.
We will prove y1 = y2.
We prove the intermediate claim Hhinj: ∀u v ∈ X, h u = h v → u = v.
An exact proof term for the current goal is (andER (∀u ∈ X, h u ∈ ω) (∀u v ∈ X, h u = h v → u = v) Hh).
Apply (ReplE_impred X F y1 Hy1) to the current goal.
Let x1 be given.
Assume Hx1X: x1 ∈ X.
Assume Hy1Fx1: y1 = F x1.
Apply (ReplE_impred X F y2 Hy2) to the current goal.
Let x2 be given.
Assume Hx2X: x2 ∈ X.
Assume Hy2Fx2: y2 = F x2.
We prove the intermediate claim Hpre1: pre y1 ∈ X ∧ y1 = F (pre y1).
An exact proof term for the current goal is (Eps_i_ax (λx0 ⇒ x0 ∈ X ∧ y1 = F x0) x1 (andI (x1 ∈ X) (y1 = F x1) Hx1X Hy1Fx1)).
We prove the intermediate claim Hpre2: pre y2 ∈ X ∧ y2 = F (pre y2).
An exact proof term for the current goal is (Eps_i_ax (λx0 ⇒ x0 ∈ X ∧ y2 = F x0) x2 (andI (x2 ∈ X) (y2 = F x2) Hx2X Hy2Fx2)).
We prove the intermediate claim Hpre1X: pre y1 ∈ X.
An exact proof term for the current goal is (andEL (pre y1 ∈ X) (y1 = F (pre y1)) Hpre1).
We prove the intermediate claim Hpre2X: pre y2 ∈ X.
An exact proof term for the current goal is (andEL (pre y2 ∈ X) (y2 = F (pre y2)) Hpre2).
We prove the intermediate claim Hg1: g y1 = h (pre y1).
Use reflexivity.
We prove the intermediate claim Hg2: g y2 = h (pre y2).
Use reflexivity.
We prove the intermediate claim Heqh: h (pre y1) = h (pre y2).
rewrite the current goal using Hg1 (from right to left).
rewrite the current goal using Hg2 (from right to left).
An exact proof term for the current goal is Hg.
We prove the intermediate claim Heqpre: pre y1 = pre y2.
An exact proof term for the current goal is (Hhinj (pre y1) Hpre1X (pre y2) Hpre2X Heqh).
We prove the intermediate claim Hy1pre: y1 = F (pre y1).
An exact proof term for the current goal is (andER (pre y1 ∈ X) (y1 = F (pre y1)) Hpre1).
We prove the intermediate claim Hy2pre: y2 = F (pre y2).
An exact proof term for the current goal is (andER (pre y2 ∈ X) (y2 = F (pre y2)) Hpre2).
rewrite the current goal using Hy1pre (from left to right).
rewrite the current goal using Hy2pre (from left to right).
rewrite the current goal using Heqpre (from left to right).
Use reflexivity.
∎