Assume HsepIm: ∃U V : set, U ∈ Tim ∧ V ∈ Tim ∧ separation_of Im U V.

We will prove False.

Apply HsepIm to the current goal.

Let U be given.

Assume HexV: ∃V : set, U ∈ Tim ∧ V ∈ Tim ∧ separation_of Im U V.

Apply HexV to the current goal.

Let V be given.

Assume HUV: U ∈ Tim ∧ V ∈ Tim ∧ separation_of Im U V.

We prove the intermediate claim HUV0: U ∈ Tim ∧ V ∈ Tim.

An exact proof term for the current goal is (andEL (U ∈ Tim ∧ V ∈ Tim) (separation_of Im U V) HUV).

We prove the intermediate claim HUin: U ∈ Tim.

An exact proof term for the current goal is (andEL (U ∈ Tim) (V ∈ Tim) HUV0).

We prove the intermediate claim HVin: V ∈ Tim.

An exact proof term for the current goal is (andER (U ∈ Tim) (V ∈ Tim) HUV0).

We prove the intermediate claim HsepUV: separation_of Im U V.

An exact proof term for the current goal is (andER (U ∈ Tim ∧ V ∈ Tim) (separation_of Im U V) HUV).

We prove the intermediate claim HUrep: ∃U0 ∈ Ty, U = U0 ∩ Im.

An exact proof term for the current goal is (SepE2 (𝒫 Im) (λW : set ⇒ ∃U0 ∈ Ty, W = U0 ∩ Im) U HUin).

We prove the intermediate claim HVrep: ∃V0 ∈ Ty, V = V0 ∩ Im.

An exact proof term for the current goal is (SepE2 (𝒫 Im) (λW : set ⇒ ∃V0 ∈ Ty, W = V0 ∩ Im) V HVin).

Apply HUrep to the current goal.

Let U0 be given.

Assume HU0pair.

We prove the intermediate claim HU0: U0 ∈ Ty.

An exact proof term for the current goal is (andEL (U0 ∈ Ty) (U = U0 ∩ Im) HU0pair).

We prove the intermediate claim HUeq: U = U0 ∩ Im.

An exact proof term for the current goal is (andER (U0 ∈ Ty) (U = U0 ∩ Im) HU0pair).

Apply HVrep to the current goal.

Let V0 be given.

Assume HV0pair.

We prove the intermediate claim HV0: V0 ∈ Ty.

An exact proof term for the current goal is (andEL (V0 ∈ Ty) (V = V0 ∩ Im) HV0pair).

We prove the intermediate claim HVeql: V = V0 ∩ Im.

An exact proof term for the current goal is (andER (V0 ∈ Ty) (V = V0 ∩ Im) HV0pair).

Set preU to be the term preimage_of X f U0.

Set preV to be the term preimage_of X f V0.

We prove the intermediate claim HpreU: preU ∈ Tx.

An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hf U0 HU0).

We prove the intermediate claim HpreV: preV ∈ Tx.

An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hf V0 HV0).

We prove the intermediate claim HsepX: separation_of X preU preV.

We prove the intermediate claim HsepL1: ((((U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).

An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = Im) HsepUV).

We prove the intermediate claim Hunion: U ∪ V = Im.

An exact proof term for the current goal is (andER ((((U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = Im) HsepUV).

We prove the intermediate claim HsepL2: (((U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty) ∧ U ≠ Empty).

An exact proof term for the current goal is (andEL (((U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) HsepL1).

We prove the intermediate claim HVne: V ≠ Empty.

An exact proof term for the current goal is (andER (((U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) HsepL1).

We prove the intermediate claim HsepL3: (U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty.

An exact proof term for the current goal is (andEL ((U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty) (U ≠ Empty) HsepL2).

We prove the intermediate claim HUne: U ≠ Empty.

An exact proof term for the current goal is (andER ((U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) ∧ U ∩ V = Empty) (U ≠ Empty) HsepL2).

We prove the intermediate claim Hpow: U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im.

An exact proof term for the current goal is (andEL (U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) (U ∩ V = Empty) HsepL3).

We prove the intermediate claim Hdisj: U ∩ V = Empty.

An exact proof term for the current goal is (andER (U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im) (U ∩ V = Empty) HsepL3).

We prove the intermediate claim HU0pow: U ∈ 𝒫 Im.

An exact proof term for the current goal is (andEL (U ∈ 𝒫 Im) (V ∈ 𝒫 Im) Hpow).

We prove the intermediate claim HV0pow: V ∈ 𝒫 Im.

An exact proof term for the current goal is (andER (U ∈ 𝒫 Im) (V ∈ 𝒫 Im) Hpow).

We prove the intermediate claim HpreUsubX: preU ⊆ X.

Let x be given.

Assume Hx: x ∈ preU.

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

We prove the intermediate claim HpreVsubX: preV ⊆ X.

Let x be given.

Assume Hx: x ∈ preV.

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

We prove the intermediate claim HpreUPow: preU ∈ 𝒫 X.

An exact proof term for the current goal is (PowerI X preU HpreUsubX).

We prove the intermediate claim HpreVPow: preV ∈ 𝒫 X.

An exact proof term for the current goal is (PowerI X preV HpreVsubX).

We prove the intermediate claim HdisjPre: preU ∩ preV = Empty.

Apply Empty_eq to the current goal.

Let x be given.

Assume Hx: x ∈ preU ∩ preV.

Apply (binintersectE preU preV x Hx) to the current goal.

Assume HxU: x ∈ preU.

Assume HxV: x ∈ preV.

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 ∈ U0) x HxU).

We prove the intermediate claim HfxU0: apply_fun f x ∈ U0.

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

We prove the intermediate claim HfxV0: apply_fun f x ∈ V0.

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

We prove the intermediate claim HfxIm: apply_fun f x ∈ Im.

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

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

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

An exact proof term for the current goal is (binintersectI U0 Im (apply_fun f x) HfxU0 HfxIm).

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

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

An exact proof term for the current goal is (binintersectI V0 Im (apply_fun f x) HfxV0 HfxIm).

We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∩ V.

An exact proof term for the current goal is (binintersectI U V (apply_fun f x) HfxU HfxV).

We prove the intermediate claim HfxE: apply_fun f x ∈ Empty.

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

An exact proof term for the current goal is HfxUV.

An exact proof term for the current goal is (EmptyE (apply_fun f x) HfxE).

We prove the intermediate claim HpreUne: preU ≠ Empty.

Apply (nonempty_has_element U HUne) to the current goal.

Let y be given.

Assume HyU: y ∈ U.

We prove the intermediate claim HUsubIm: U ⊆ Im.

An exact proof term for the current goal is (PowerE Im U HU0pow).

We prove the intermediate claim HyIm: y ∈ Im.

An exact proof term for the current goal is (HUsubIm y HyU).

Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) y HyIm) to the current goal.

Let x be given.

Assume HxX: x ∈ X.

Assume Hyx: y = apply_fun f x.

We prove the intermediate claim HyU0Im: y ∈ U0 ∩ Im.

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

An exact proof term for the current goal is HyU.

We prove the intermediate claim HyU0: y ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 Im y HyU0Im).

We prove the intermediate claim HfxU0: apply_fun f x ∈ U0.

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

An exact proof term for the current goal is HyU0.

We prove the intermediate claim HxPreU: x ∈ preU.

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

An exact proof term for the current goal is (elem_implies_nonempty preU x HxPreU).

We prove the intermediate claim HpreVne: preV ≠ Empty.

Apply (nonempty_has_element V HVne) to the current goal.

Let y be given.

Assume HyV: y ∈ V.

We prove the intermediate claim HVsubIm: V ⊆ Im.

An exact proof term for the current goal is (PowerE Im V HV0pow).

We prove the intermediate claim HyIm: y ∈ Im.

An exact proof term for the current goal is (HVsubIm y HyV).

Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) y HyIm) to the current goal.

Let x be given.

Assume HxX: x ∈ X.

Assume Hyx: y = apply_fun f x.

We prove the intermediate claim HyV0Im: y ∈ V0 ∩ Im.

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

An exact proof term for the current goal is HyV.

We prove the intermediate claim HyV0: y ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 Im y HyV0Im).

We prove the intermediate claim HfxV0: apply_fun f x ∈ V0.

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

An exact proof term for the current goal is HyV0.

We prove the intermediate claim HxPreV: x ∈ preV.

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

An exact proof term for the current goal is (elem_implies_nonempty preV x HxPreV).

We prove the intermediate claim HunionPre: preU ∪ preV = X.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ preU ∪ preV.

Apply (binunionE preU preV x Hx) to the current goal.

Assume HxU: x ∈ preU.

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

Assume HxV: x ∈ preV.

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

Let x be given.

Assume HxX: x ∈ X.

We will prove x ∈ preU ∪ preV.

We prove the intermediate claim HfxIm: apply_fun f x ∈ Im.

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

We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∪ V.

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

An exact proof term for the current goal is HfxIm.

Apply (binunionE U V (apply_fun f x) HfxUV) to the current goal.

Assume HfxU: apply_fun f x ∈ U.

We prove the intermediate claim HfxU0Im: apply_fun f x ∈ U0 ∩ Im.

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

An exact proof term for the current goal is HfxU.

We prove the intermediate claim HfxU0: apply_fun f x ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 Im (apply_fun f x) HfxU0Im).

An exact proof term for the current goal is (binunionI1 preU preV x (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U0) x HxX HfxU0)).

Assume HfxV: apply_fun f x ∈ V.

We prove the intermediate claim HfxV0Im: apply_fun f x ∈ V0 ∩ Im.

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

An exact proof term for the current goal is HfxV.

We prove the intermediate claim HfxV0: apply_fun f x ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 Im (apply_fun f x) HfxV0Im).

An exact proof term for the current goal is (binunionI2 preU preV x (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ V0) x HxX HfxV0)).

We will prove (((((preU ∈ 𝒫 X ∧ preV ∈ 𝒫 X) ∧ preU ∩ preV = Empty) ∧ preU ≠ Empty) ∧ preV ≠ Empty) ∧ preU ∪ preV = X).

Apply andI to the current goal.

An exact proof term for the current goal is HpreUPow.

An exact proof term for the current goal is HpreVPow.

An exact proof term for the current goal is HdisjPre.

An exact proof term for the current goal is HpreUne.

An exact proof term for the current goal is HpreVne.

An exact proof term for the current goal is HunionPre.

Apply HnoSepX to the current goal.

We use preU to witness the existential quantifier.

We use preV to witness the existential quantifier.

We will prove preU ∈ Tx ∧ preV ∈ Tx ∧ separation_of X preU preV.

Apply andI to the current goal.

An exact proof term for the current goal is HpreU.

An exact proof term for the current goal is HpreV.

An exact proof term for the current goal is HsepX.