Let X and y be given.

Assume HX: finite X.

Assume Hy: y ∉ X.

Assume IH: finite {f x|x ∈ X}.

We will prove finite {f x|x ∈ X ∪ {y}}.

We prove the intermediate claim L1: {f x|x ∈ X ∪ {y}} = {f x|x ∈ X} ∪ {f y}.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ {f x|x ∈ X ∪ {y}}.

Apply ReplE_impred (X ∪ {y}) f z Hz to the current goal.

Let x be given.

Assume Hx: x ∈ X ∪ {y}.

Assume Hzx: z = f x.

We will prove z ∈ {f x|x ∈ X} ∪ {f y}.

Apply binunionE X {y} x Hx to the current goal.

Assume H1: x ∈ X.

Apply binunionI1 to the current goal.

rewrite the current goal using Hzx (from left to right).

An exact proof term for the current goal is ReplI X f x H1.

Assume H1: x ∈ {y}.

Apply binunionI2 to the current goal.

rewrite the current goal using Hzx (from left to right).

rewrite the current goal using SingE y x H1 (from left to right).

Apply SingI to the current goal.

Let z be given.

Assume Hz: z ∈ {f x|x ∈ X} ∪ {f y}.

Apply binunionE {f x|x ∈ X} {f y} z Hz to the current goal.

Assume H1: z ∈ {f x|x ∈ X}.

Apply ReplE_impred X f z H1 to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume Hzx: z = f x.

rewrite the current goal using Hzx (from left to right).

Apply ReplI to the current goal.

We will prove x ∈ X ∪ {y}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hx.

Assume H1: z ∈ {f y}.

rewrite the current goal using SingE (f y) z H1 (from left to right).

We will prove f y ∈ {f x|x ∈ X ∪ {y}}.

Apply ReplI to the current goal.

Apply binunionI2 to the current goal.

We will prove y ∈ {y}.

Apply SingI to the current goal.

rewrite the current goal using L1 (from left to right).

Apply binunion_finite to the current goal.

An exact proof term for the current goal is IH.

Apply Sing_finite to the current goal.