Let y be given.

Assume Hy: y ∈ image_of f (⋃ Fam).

We will prove y ∈ ⋃ {image_of f U|U ∈ Fam}.

Apply (ReplE_impred (⋃ Fam) (λx : set ⇒ apply_fun f x) y Hy) to the current goal.

Let x be given.

Assume HxU: x ∈ ⋃ Fam.

Assume Hyx: y = apply_fun f x.

Apply (UnionE_impred Fam x HxU) to the current goal.

Let U be given.

Assume HxUin: x ∈ U.

Assume HUFam: U ∈ Fam.

We prove the intermediate claim HyImU: y ∈ image_of f U.

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

An exact proof term for the current goal is (ReplI U (λx0 : set ⇒ apply_fun f x0) x HxUin).

An exact proof term for the current goal is (UnionI {image_of f U0|U0 ∈ Fam} y (image_of f U) HyImU (ReplI Fam (λU0 : set ⇒ image_of f U0) U HUFam)).

Let y be given.

Assume Hy: y ∈ ⋃ {image_of f U|U ∈ Fam}.

We will prove y ∈ image_of f (⋃ Fam).

Apply (UnionE_impred {image_of f U|U ∈ Fam} y Hy) to the current goal.

Let W be given.

Assume HyW: y ∈ W.

Assume HW: W ∈ {image_of f U|U ∈ Fam}.

Apply (ReplE_impred Fam (λU0 : set ⇒ image_of f U0) W HW) to the current goal.

Let U be given.

Assume HUFam: U ∈ Fam.

Assume HWU: W = image_of f U.

We prove the intermediate claim HyImU: y ∈ image_of f U.

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

An exact proof term for the current goal is HyW.

Apply (ReplE_impred U (λx : set ⇒ apply_fun f x) y HyImU) to the current goal.

Let x be given.

Assume HxU: x ∈ U.

Assume Hyx: y = apply_fun f x.

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

An exact proof term for the current goal is (ReplI (⋃ Fam) (λx0 : set ⇒ apply_fun f x0) x (UnionI Fam x U HxU HUFam)).