Let x be given.

Assume Hx: x ∈ preimage_of X f (⋃ Fam).

We will prove x ∈ ⋃ {preimage_of X f V|V ∈ Fam}.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ ⋃ Fam) x Hx).

We prove the intermediate claim HfxU: apply_fun f x ∈ ⋃ Fam.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ ⋃ Fam) x Hx).

Apply (UnionE_impred Fam (apply_fun f x) HfxU) to the current goal.

Let V be given.

Assume HfxV: apply_fun f x ∈ V.

Assume HVFam: V ∈ Fam.

We prove the intermediate claim HxPre: x ∈ preimage_of X f V.

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxX HfxV).

An exact proof term for the current goal is (UnionI {preimage_of X f V0|V0 ∈ Fam} x (preimage_of X f V) HxPre (ReplI Fam (λV0 : set ⇒ preimage_of X f V0) V HVFam)).

Let x be given.

Assume Hx: x ∈ ⋃ {preimage_of X f V|V ∈ Fam}.

We will prove x ∈ preimage_of X f (⋃ Fam).

Apply (UnionE_impred {preimage_of X f V|V ∈ Fam} x Hx) to the current goal.

Let W be given.

Assume HxW: x ∈ W.

Assume HW: W ∈ {preimage_of X f V|V ∈ Fam}.

Apply (ReplE_impred Fam (λV0 : set ⇒ preimage_of X f V0) W HW) to the current goal.

Let V be given.

Assume HVFam: V ∈ Fam.

Assume HWV: W = preimage_of X f V.

We prove the intermediate claim HxPre: x ∈ preimage_of X f V.

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

An exact proof term for the current goal is HxW.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPre).

We prove the intermediate claim HfxV: apply_fun f x ∈ V.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPre).

We prove the intermediate claim HfxU: apply_fun f x ∈ ⋃ Fam.

An exact proof term for the current goal is (UnionI Fam (apply_fun f x) V HfxV HVFam).

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ ⋃ Fam) x HxX HfxU).