Assume HsepY: ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ separation_of Y U V.

We will prove False.

We prove the intermediate claim HnoSepX: ¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V).

An exact proof term for the current goal is (connected_space_no_separation X Tx HX).

We prove the intermediate claim Hcontf: continuous_map X Tx Y Ty f.

An exact proof term for the current goal is (andEL (continuous_map X Tx Y Ty f) (∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y)) Hhom).

We prove the intermediate claim Habc: (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y.

An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hcontf).

We prove the intermediate claim Hfunf: function_on f X Y.

An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Habc).

We prove the intermediate claim Hpreimg: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.

An exact proof term for the current goal is (andER ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hcontf).

We prove the intermediate claim Hexg: ∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y).

An exact proof term for the current goal is (andER (continuous_map X Tx Y Ty f) (∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y)) Hhom).

Apply Hexg to the current goal.

Let g be given.

Assume Hgprop.

We prove the intermediate claim Hfg: ∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y.

An exact proof term for the current goal is (andER (continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x)) (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y) Hgprop).

We prove the intermediate claim Habg: continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x).

An exact proof term for the current goal is (andEL (continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x)) (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y) Hgprop).

We prove the intermediate claim Hcontg: continuous_map Y Ty X Tx g.

An exact proof term for the current goal is (andEL (continuous_map Y Ty X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) Habg).

We prove the intermediate claim Habcg: (topology_on Y Ty ∧ topology_on X Tx) ∧ function_on g Y X.

An exact proof term for the current goal is (andEL ((topology_on Y Ty ∧ topology_on X Tx) ∧ function_on g Y X) (∀V : set, V ∈ Tx → preimage_of Y g V ∈ Ty) Hcontg).

We prove the intermediate claim Hfung: function_on g Y X.

An exact proof term for the current goal is (andER (topology_on Y Ty ∧ topology_on X Tx) (function_on g Y X) Habcg).

Apply HsepY to the current goal.

Let U be given.

Assume HexV: ∃V : set, U ∈ Ty ∧ V ∈ Ty ∧ separation_of Y U V.

Apply HexV to the current goal.

Let V be given.

Assume HUV: U ∈ Ty ∧ V ∈ Ty ∧ separation_of Y U V.

Set U0 to be the term preimage_of X f U.

Set V0 to be the term preimage_of X f V.

We prove the intermediate claim HUVop: U ∈ Ty ∧ V ∈ Ty.

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

We prove the intermediate claim HU_Ty: U ∈ Ty.

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

We prove the intermediate claim HV_Ty: V ∈ Ty.

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

We prove the intermediate claim HsepYUV: separation_of Y U V.

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

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (Hpreimg U HU_Ty).

We prove the intermediate claim HV0Tx: V0 ∈ Tx.

An exact proof term for the current goal is (Hpreimg V HV_Ty).

We prove the intermediate claim HsepXUV: separation_of X U0 V0.

We will prove U0 ∈ 𝒫 X ∧ V0 ∈ 𝒫 X ∧ U0 ∩ V0 = Empty ∧ U0 ≠ Empty ∧ V0 ≠ Empty ∧ U0 ∪ V0 = X.

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

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

We prove the intermediate claim HcoverY: U ∪ V = Y.

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

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

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

We prove the intermediate claim HVne: V ≠ Empty.

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

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

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

We prove the intermediate claim HUne: U ≠ Empty.

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

We prove the intermediate claim HUVpow: U ∈ 𝒫 Y ∧ V ∈ 𝒫 Y.

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

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

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

We prove the intermediate claim HUpow: U ∈ 𝒫 Y.

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

We prove the intermediate claim HVpow: V ∈ 𝒫 Y.

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

We prove the intermediate claim HU0subX: U0 ⊆ X.

Let x be given.

Assume Hx: x ∈ U0.

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

We prove the intermediate claim HV0subX: V0 ⊆ X.

Let x be given.

Assume Hx: x ∈ V0.

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

We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 X.

An exact proof term for the current goal is (PowerI X U0 HU0subX).

We prove the intermediate claim HV0Pow: V0 ∈ 𝒫 X.

An exact proof term for the current goal is (PowerI X V0 HV0subX).

We prove the intermediate claim Hdisj: U0 ∩ V0 = Empty.

rewrite the current goal using (preimage_of_binintersect X f U V) (from right to left).

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

An exact proof term for the current goal is (preimage_of_Empty X f).

We prove the intermediate claim HU0ne: U0 ≠ Empty.

Apply (nonempty_has_element U HUne) to the current goal.

Let y be given.

Assume HyU: y ∈ U.

We prove the intermediate claim HUsubY: U ⊆ Y.

An exact proof term for the current goal is (PowerE Y U HUpow).

We prove the intermediate claim HyY: y ∈ Y.

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

We prove the intermediate claim HgyX: apply_fun g y ∈ X.

An exact proof term for the current goal is (Hfung y HyY).

We prove the intermediate claim HfgyU: apply_fun f (apply_fun g y) ∈ U.

rewrite the current goal using (Hfg y HyY) (from left to right).

An exact proof term for the current goal is HyU.

We prove the intermediate claim HgyPreU: apply_fun g y ∈ U0.

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U) (apply_fun g y) HgyX HfgyU).

An exact proof term for the current goal is (elem_implies_nonempty U0 (apply_fun g y) HgyPreU).

We prove the intermediate claim HV0ne: V0 ≠ Empty.

Apply (nonempty_has_element V HVne) to the current goal.

Let y be given.

Assume HyV: y ∈ V.

We prove the intermediate claim HVsubY: V ⊆ Y.

An exact proof term for the current goal is (PowerE Y V HVpow).

We prove the intermediate claim HyY: y ∈ Y.

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

We prove the intermediate claim HgyX: apply_fun g y ∈ X.

An exact proof term for the current goal is (Hfung y HyY).

We prove the intermediate claim HfgyV: apply_fun f (apply_fun g y) ∈ V.

rewrite the current goal using (Hfg y HyY) (from left to right).

An exact proof term for the current goal is HyV.

We prove the intermediate claim HgyPreV: apply_fun g y ∈ V0.

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ V) (apply_fun g y) HgyX HfgyV).

An exact proof term for the current goal is (elem_implies_nonempty V0 (apply_fun g y) HgyPreV).

We prove the intermediate claim Hunion: U0 ∪ V0 = X.

rewrite the current goal using (preimage_of_binunion X f U V) (from right to left).

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

An exact proof term for the current goal is (preimage_of_whole X Y f Hfunf).

We will prove (((((U0 ∈ 𝒫 X ∧ V0 ∈ 𝒫 X) ∧ U0 ∩ V0 = Empty) ∧ U0 ≠ Empty) ∧ V0 ≠ Empty) ∧ U0 ∪ V0 = X).

Apply andI to the current goal.

An exact proof term for the current goal is HU0Pow.

An exact proof term for the current goal is HV0Pow.

An exact proof term for the current goal is Hdisj.

An exact proof term for the current goal is HU0ne.

An exact proof term for the current goal is HV0ne.

An exact proof term for the current goal is Hunion.

Apply HnoSepX to the current goal.

We use U0 to witness the existential quantifier.

We use V0 to witness the existential quantifier.

We will prove U0 ∈ Tx ∧ V0 ∈ Tx ∧ separation_of X U0 V0.

Apply andI to the current goal.

An exact proof term for the current goal is HU0Tx.

An exact proof term for the current goal is HV0Tx.

An exact proof term for the current goal is HsepXUV.