We will prove homeomorphism X Tx Im Tim f.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (continuous_map_topology_dom X Tx Y Ty f Hcont).

We prove the intermediate claim HTy: topology_on Y Ty.

An exact proof term for the current goal is (continuous_map_topology_cod X Tx Y Ty f Hcont).

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

An exact proof term for the current goal is (continuous_map_function_on X Tx Y Ty f Hcont).

We prove the intermediate claim HImsubY: Im ⊆ Y.

An exact proof term for the current goal is (image_of_sub_codomain f X Y X HfunXY (Subq_ref X)).

We prove the intermediate claim HimgIm: ∀x : set, x ∈ X → apply_fun f x ∈ Im.

Let x be given.

Assume HxX: x ∈ X.

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

We prove the intermediate claim HcontIm: continuous_map X Tx Im Tim f.

An exact proof term for the current goal is (continuous_map_range_restrict X Tx Y Ty f Im Hcont HImsubY HimgIm).

Set gx to be the term (λy : set ⇒ Eps_i (λx : set ⇒ x ∈ X ∧ apply_fun f x = y)).

Set g to be the term graph Im (λy : set ⇒ gx y).

We prove the intermediate claim Hgfun: function_on g Im X.

Let y be given.

Assume HyIm: y ∈ Im.

rewrite the current goal using (apply_fun_graph Im (λy0 : set ⇒ gx y0) y HyIm) (from left to right).

We prove the intermediate claim Hex: ∃x : set, x ∈ X ∧ apply_fun f x = y.

Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) y HyIm (∃x : set, x ∈ X ∧ apply_fun f x = y)) to the current goal.

Let x be given.

Assume HxX: x ∈ X.

Assume Hyeq: y = apply_fun f x.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxX.

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

Use reflexivity.

We prove the intermediate claim Hgx: gx y ∈ X ∧ apply_fun f (gx y) = y.

An exact proof term for the current goal is (Eps_i_ex (λx : set ⇒ x ∈ X ∧ apply_fun f x = y) Hex).

An exact proof term for the current goal is (andEL (gx y ∈ X) (apply_fun f (gx y) = y) Hgx).

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

Let y be given.

Assume HyIm: y ∈ Im.

We prove the intermediate claim Hex: ∃x : set, x ∈ X ∧ apply_fun f x = y.

Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) y HyIm (∃x : set, x ∈ X ∧ apply_fun f x = y)) to the current goal.

Let x be given.

Assume HxX: x ∈ X.

Assume Hyeq: y = apply_fun f x.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxX.

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

Use reflexivity.

We prove the intermediate claim HgyDef: apply_fun g y = gx y.

We prove the intermediate claim Hgdef: g = graph Im (λy0 : set ⇒ gx y0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph Im (λy0 : set ⇒ gx y0) y HyIm).

rewrite the current goal using HgyDef (from left to right) at position 1.

We prove the intermediate claim Hgx: gx y ∈ X ∧ apply_fun f (gx y) = y.

An exact proof term for the current goal is (Eps_i_ex (λx : set ⇒ x ∈ X ∧ apply_fun f x = y) Hex).

An exact proof term for the current goal is (andER (gx y ∈ X) (apply_fun f (gx y) = y) Hgx).

We prove the intermediate claim Hgcont: continuous_map Im Tim X Tx g.

We will prove topology_on Im Tim ∧ topology_on X Tx ∧ function_on g Im X ∧ ∀U : set, U ∈ Tx → preimage_of Im g U ∈ Tim.

Apply andI to the current goal.

An exact proof term for the current goal is (subspace_topology_is_topology Y Ty Im HTy HImsubY).

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is Hgfun.

Let U be given.

Assume HU: U ∈ Tx.

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HU).

Set pick to be the term (λx : set ⇒ Eps_i (λV : set ⇒ V ∈ Ty ∧ apply_fun f x ∈ V ∧ preimage_of X f V ⊆ U)).

Set pickf to be the term graph U (λx : set ⇒ pick x).

Set Fam to be the term image_of pickf U.

Set VU to be the term ⋃ Fam.

We prove the intermediate claim HpickTy: ∀x : set, x ∈ U → pick x ∈ Ty ∧ apply_fun f x ∈ pick x ∧ preimage_of X f (pick x) ⊆ U.

Let x be given.

Assume HxU: x ∈ U.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HUsubX x HxU).

We prove the intermediate claim HexV: ∃V : set, V ∈ Ty ∧ apply_fun f x ∈ V ∧ preimage_of X f V ⊆ U.

An exact proof term for the current goal is (Hloc x U HxX HU HxU).

An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ V ∈ Ty ∧ apply_fun f x ∈ V ∧ preimage_of X f V ⊆ U) HexV).

We prove the intermediate claim HFamPow: Fam ∈ 𝒫 Ty.

Apply PowerI to the current goal.

Let V be given.

Assume HVFam: V ∈ Fam.

We will prove V ∈ Ty.

Apply (ReplE_impred U (λx0 : set ⇒ apply_fun pickf x0) V HVFam (V ∈ Ty)) to the current goal.

Let x be given.

Assume HxU: x ∈ U.

Assume HVeq: V = apply_fun pickf x.

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

We prove the intermediate claim Hpf: apply_fun pickf x = pick x.

We prove the intermediate claim Hpfdef: pickf = graph U (λx0 : set ⇒ pick x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph U (λx0 : set ⇒ pick x0) x HxU).

rewrite the current goal using Hpf (from left to right) at position 1.

We prove the intermediate claim Hp12: pick x ∈ Ty ∧ apply_fun f x ∈ pick x.

An exact proof term for the current goal is (andEL (pick x ∈ Ty ∧ apply_fun f x ∈ pick x) (preimage_of X f (pick x) ⊆ U) (HpickTy x HxU)).

An exact proof term for the current goal is (andEL (pick x ∈ Ty) (apply_fun f x ∈ pick x) Hp12).

We prove the intermediate claim HVUopen: VU ∈ Ty.

An exact proof term for the current goal is (topology_union_closed_pow Y Ty Fam HTy HFamPow).

We prove the intermediate claim HpreEq: preimage_of Im g U = (VU ∩ Im).

Apply set_ext to the current goal.

Let y be given.

Assume HyPre: y ∈ preimage_of Im g U.

We will prove y ∈ VU ∩ Im.

We prove the intermediate claim HyIm: y ∈ Im.

An exact proof term for the current goal is (SepE1 Im (λy0 : set ⇒ apply_fun g y0 ∈ U) y HyPre).

We prove the intermediate claim HgyU: apply_fun g y ∈ U.

An exact proof term for the current goal is (SepE2 Im (λy0 : set ⇒ apply_fun g y0 ∈ U) y HyPre).

Apply binintersectI to the current goal.

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

An exact proof term for the current goal is (Hgfun y HyIm).

We prove the intermediate claim HyEq: apply_fun f (apply_fun g y) = y.

An exact proof term for the current goal is (Hgfmap y HyIm).

Set x to be the term apply_fun g y.

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is HgyU.

We prove the intermediate claim Hp: pick x ∈ Ty ∧ apply_fun f x ∈ pick x ∧ preimage_of X f (pick x) ⊆ U.

An exact proof term for the current goal is (HpickTy x HxU).

We prove the intermediate claim HyInPick: y ∈ pick x.

We prove the intermediate claim Hp12: pick x ∈ Ty ∧ apply_fun f x ∈ pick x.

An exact proof term for the current goal is (andEL (pick x ∈ Ty ∧ apply_fun f x ∈ pick x) (preimage_of X f (pick x) ⊆ U) Hp).

We prove the intermediate claim HfxIn: apply_fun f x ∈ pick x.

An exact proof term for the current goal is (andER (pick x ∈ Ty) (apply_fun f x ∈ pick x) Hp12).

We prove the intermediate claim HyEq2: apply_fun f x = y.

We prove the intermediate claim Hxdef: x = apply_fun g y.

Use reflexivity.

rewrite the current goal using Hxdef (from left to right) at position 1.

An exact proof term for the current goal is HyEq.

rewrite the current goal using HyEq2 (from right to left) at position 1.

An exact proof term for the current goal is HfxIn.

We prove the intermediate claim HpickInFam: pick x ∈ Fam.

We prove the intermediate claim Htmp: apply_fun pickf x ∈ Fam.

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

We prove the intermediate claim Hpf: apply_fun pickf x = pick x.

We prove the intermediate claim Hpfdef: pickf = graph U (λx0 : set ⇒ pick x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph U (λx0 : set ⇒ pick x0) x HxU).

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

An exact proof term for the current goal is Htmp.

An exact proof term for the current goal is (UnionI Fam y (pick x) HyInPick HpickInFam).

An exact proof term for the current goal is HyIm.

Let y be given.

Assume HyInt: y ∈ VU ∩ Im.

We will prove y ∈ preimage_of Im g U.

We prove the intermediate claim HyVU: y ∈ VU.

An exact proof term for the current goal is (binintersectE1 VU Im y HyInt).

We prove the intermediate claim HyIm: y ∈ Im.

An exact proof term for the current goal is (binintersectE2 VU Im y HyInt).

Apply (UnionE_impred Fam y HyVU (y ∈ preimage_of Im g U)) to the current goal.

Let V be given.

Assume HyV: y ∈ V.

Assume HVFam: V ∈ Fam.

Apply (ReplE_impred U (λx0 : set ⇒ apply_fun pickf x0) V HVFam (y ∈ preimage_of Im g U)) to the current goal.

Let x be given.

Assume HxU: x ∈ U.

Assume HVe: V = apply_fun pickf x.

We prove the intermediate claim Hpf: apply_fun pickf x = pick x.

We prove the intermediate claim Hpfdef: pickf = graph U (λx0 : set ⇒ pick x0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph U (λx0 : set ⇒ pick x0) x HxU).

We prove the intermediate claim HVe2: V = pick x.

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

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

Use reflexivity.

We prove the intermediate claim Hp: pick x ∈ Ty ∧ apply_fun f x ∈ pick x ∧ preimage_of X f (pick x) ⊆ U.

An exact proof term for the current goal is (HpickTy x HxU).

We prove the intermediate claim HpreSub: preimage_of X f (pick x) ⊆ U.

An exact proof term for the current goal is (andER (pick x ∈ Ty ∧ apply_fun f x ∈ pick x) (preimage_of X f (pick x) ⊆ U) Hp).

We prove the intermediate claim HyPick: y ∈ pick x.

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

An exact proof term for the current goal is HyV.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HUsubX x HxU).

We prove the intermediate claim Hyfx: apply_fun f x ∈ pick x.

We prove the intermediate claim Hp12: pick x ∈ Ty ∧ apply_fun f x ∈ pick x.

An exact proof term for the current goal is (andEL (pick x ∈ Ty ∧ apply_fun f x ∈ pick x) (preimage_of X f (pick x) ⊆ U) Hp).

An exact proof term for the current goal is (andER (pick x ∈ Ty) (apply_fun f x ∈ pick x) Hp12).

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

An exact proof term for the current goal is (Hgfun y HyIm).

We prove the intermediate claim HyEq: apply_fun f (apply_fun g y) = y.

An exact proof term for the current goal is (Hgfmap y HyIm).

We prove the intermediate claim HgyPre: apply_fun g y ∈ preimage_of X f (pick x).

We prove the intermediate claim HfgyPick: apply_fun f (apply_fun g y) ∈ pick x.

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

An exact proof term for the current goal is HyPick.

An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ pick x) (apply_fun g y) HgyX HfgyPick).

We prove the intermediate claim HgyU: apply_fun g y ∈ U.

An exact proof term for the current goal is (HpreSub (apply_fun g y) HgyPre).

An exact proof term for the current goal is (SepI Im (λy0 : set ⇒ apply_fun g y0 ∈ U) y HyIm HgyU).

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

We prove the intermediate claim Hopen: open_in Im Tim (VU ∩ Im).

We prove the intermediate claim HcapSub: (VU ∩ Im) ⊆ Im.

Let z be given.

Assume Hz: z ∈ VU ∩ Im.

An exact proof term for the current goal is (binintersectE2 VU Im z Hz).

We prove the intermediate claim HTimdef: Tim = subspace_topology Y Ty Im.

Use reflexivity.

rewrite the current goal using HTimdef (from left to right) at position 1.

Apply (iffER (open_in Im (subspace_topology Y Ty Im) (VU ∩ Im)) (∃V ∈ Ty, (VU ∩ Im) = V ∩ Im) (open_in_subspace_iff Y Ty Im (VU ∩ Im) HTy HImsubY HcapSub)) to the current goal.

We use VU to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HVUopen.

Use reflexivity.

An exact proof term for the current goal is (open_in_elem Im Tim (VU ∩ Im) Hopen).

We will prove (continuous_map X Tx Im Tim f ∧ ∃g0 : set, continuous_map Im Tim X Tx g0 ∧ (∀x : set, x ∈ X → apply_fun g0 (apply_fun f x) = x) ∧ (∀y : set, y ∈ Im → apply_fun f (apply_fun g0 y) = y)).

Apply andI to the current goal.

An exact proof term for the current goal is HcontIm.

We use g to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hgcont.

Let x be given.

Assume HxX: x ∈ X.

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

An exact proof term for the current goal is (HimgIm x HxX).

We prove the intermediate claim Hgf: apply_fun f (apply_fun g (apply_fun f x)) = apply_fun f x.

An exact proof term for the current goal is (Hgfmap (apply_fun f x) HfxIm).

We prove the intermediate claim HgxX: apply_fun g (apply_fun f x) ∈ X.

An exact proof term for the current goal is (Hgfun (apply_fun f x) HfxIm).

An exact proof term for the current goal is (Hinj (apply_fun g (apply_fun f x)) x HgxX HxX Hgf).

Let y be given.

Assume HyIm: y ∈ Im.

An exact proof term for the current goal is (Hgfmap y HyIm).