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 p Hcont).

We prove the intermediate claim HdefOne: one_point_sets_closed Y Ty = (topology_on Y Ty ∧ ∀y : set, y ∈ Y → closed_in Y Ty {y}).

Use reflexivity.

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

Apply andI to the current goal.

An exact proof term for the current goal is HTy.

Let y be given.

Assume HyY: y ∈ Y.

We will prove closed_in Y Ty {y}.

Apply (Hsurj y HyY) to the current goal.

Let x be given.

Assume Hxpair: x ∈ X ∧ apply_fun p x = y.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (andEL (x ∈ X) (apply_fun p x = y) Hxpair).

We prove the intermediate claim Hpx: apply_fun p x = y.

An exact proof term for the current goal is (andER (x ∈ X) (apply_fun p x = y) Hxpair).

We prove the intermediate claim HoneX: one_point_sets_closed X Tx.

An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) HnormX).

We prove the intermediate claim HsingClosedX: closed_in X Tx {x}.

We prove the intermediate claim HallSing: ∀z : set, z ∈ X → closed_in X Tx {z}.

An exact proof term for the current goal is (andER (topology_on X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) HoneX).

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

We prove the intermediate claim HimgClosedY: closed_in Y Ty (image_of p {x}).

We prove the intermediate claim HallImgClosed: ∀A0 : set, closed_in X Tx A0 → closed_in Y Ty (image_of p A0).

An exact proof term for the current goal is (andER (function_on p X Y) (∀A0 : set, closed_in X Tx A0 → closed_in Y Ty (image_of p A0)) Hclmap).

An exact proof term for the current goal is (HallImgClosed {x} HsingClosedX).

We prove the intermediate claim HimgEq: image_of p {x} = {y}.

Apply set_ext to the current goal.

Let t be given.

Assume Ht: t ∈ image_of p {x}.

We will prove t ∈ {y}.

We prove the intermediate claim Hdef: image_of p {x} = Repl {x} (λu : set ⇒ apply_fun p u).

Use reflexivity.

We prove the intermediate claim HtRepl: t ∈ Repl {x} (λu : set ⇒ apply_fun p u).

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

An exact proof term for the current goal is Ht.

Apply (ReplE_impred {x} (λu : set ⇒ apply_fun p u) t HtRepl) to the current goal.

Let u be given.

Assume Hu: u ∈ {x}.

Assume Htpu: t = apply_fun p u.

We prove the intermediate claim Hueq: u = x.

An exact proof term for the current goal is (SingE x u Hu).

We prove the intermediate claim Htpx: t = apply_fun p x.

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

An exact proof term for the current goal is Htpu.

We prove the intermediate claim Hteq: t = y.

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

An exact proof term for the current goal is Hpx.

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

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

Let t be given.

Assume Ht: t ∈ {y}.

We will prove t ∈ image_of p {x}.

We prove the intermediate claim Hteq: t = y.

An exact proof term for the current goal is (SingE y t Ht).

We prove the intermediate claim Htpx: t = apply_fun p x.

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

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

Use reflexivity.

We prove the intermediate claim Hdef: image_of p {x} = Repl {x} (λu : set ⇒ apply_fun p u).

Use reflexivity.

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

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

An exact proof term for the current goal is (ReplI {x} (λu : set ⇒ apply_fun p u) x (SingI x)).

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

An exact proof term for the current goal is HimgClosedY.

Let A and B be given.

Assume HAcl: closed_in Y Ty A.

Assume HBcl: closed_in Y Ty B.

Assume HAB: A ∩ B = Empty.

We will prove ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.

Set preA to be the term preimage_of X p A.

Set preB to be the term preimage_of X p B.

We prove the intermediate claim HpreAcl: closed_in X Tx preA.

An exact proof term for the current goal is (continuous_preserves_closed X Tx Y Ty p Hcont A HAcl).

We prove the intermediate claim HpreBcl: closed_in X Tx preB.

An exact proof term for the current goal is (continuous_preserves_closed X Tx Y Ty p Hcont B HBcl).

We prove the intermediate claim HpreDisj: preA ∩ preB = Empty.

rewrite the current goal using (preimage_of_binintersect X p A B) (from right to left).

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

rewrite the current goal using (preimage_of_Empty X p) (from left to right).

Use reflexivity.

We prove the intermediate claim HsepX: ∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty.

An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty) HnormX).

Apply (HsepX preA preB HpreAcl HpreBcl HpreDisj) to the current goal.

Let U be given.

Assume HU0.

Apply HU0 to the current goal.

Let V be given.

Assume HUVpack.

Apply (and5E (U ∈ Tx) (V ∈ Tx) (preA ⊆ U) (preB ⊆ V) (U ∩ V = Empty) HUVpack) to the current goal.

Assume HUopen HVopen HpreAsub HpreBsub HUVdisj.

Set UY to be the term Y ∖ image_of p (X ∖ U).

Set VY to be the term Y ∖ image_of p (X ∖ V).

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (normal_space_topology_on X Tx HnormX).

We prove the intermediate claim HallImgClosed: ∀A0 : set, closed_in X Tx A0 → closed_in Y Ty (image_of p A0).

An exact proof term for the current goal is (andER (function_on p X Y) (∀A0 : set, closed_in X Tx A0 → closed_in Y Ty (image_of p A0)) Hclmap).

We prove the intermediate claim HimgCompUclosed: closed_in Y Ty (image_of p (X ∖ U)).

We prove the intermediate claim HcompUclosed: closed_in X Tx (X ∖ U).

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

An exact proof term for the current goal is (HallImgClosed (X ∖ U) HcompUclosed).

We prove the intermediate claim HimgCompVclosed: closed_in Y Ty (image_of p (X ∖ V)).

We prove the intermediate claim HcompVclosed: closed_in X Tx (X ∖ V).

An exact proof term for the current goal is (closed_of_open_complement X Tx V HTx HVopen).

An exact proof term for the current goal is (HallImgClosed (X ∖ V) HcompVclosed).

We prove the intermediate claim HUYopen: UY ∈ Ty.

An exact proof term for the current goal is (open_in_elem Y Ty UY (open_of_closed_complement Y Ty (image_of p (X ∖ U)) HimgCompUclosed)).

We prove the intermediate claim HVYopen: VY ∈ Ty.

An exact proof term for the current goal is (open_in_elem Y Ty VY (open_of_closed_complement Y Ty (image_of p (X ∖ V)) HimgCompVclosed)).

We prove the intermediate claim HAsubY: A ⊆ Y.

An exact proof term for the current goal is (andEL (A ⊆ Y) (∃U0 ∈ Ty, A = Y ∖ U0) (closed_in_package Y Ty A HAcl)).

We prove the intermediate claim HBsubY: B ⊆ Y.

An exact proof term for the current goal is (andEL (B ⊆ Y) (∃U0 ∈ Ty, B = Y ∖ U0) (closed_in_package Y Ty B HBcl)).

We prove the intermediate claim HAsubUY: A ⊆ UY.

Let y be given.

Assume HyA: y ∈ A.

We will prove y ∈ UY.

We prove the intermediate claim HyY: y ∈ Y.

An exact proof term for the current goal is (HAsubY y HyA).

Apply (setminusI Y (image_of p (X ∖ U)) y HyY) to the current goal.

Assume HyImg: y ∈ image_of p (X ∖ U).

Apply (ReplE_impred (X ∖ U) (λx0 : set ⇒ apply_fun p x0) y HyImg) to the current goal.

Let x0 be given.

Assume Hx0XU: x0 ∈ (X ∖ U).

Assume Hypx0: y = apply_fun p x0.

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (setminusE1 X U x0 Hx0XU).

We prove the intermediate claim Hypx0A: apply_fun p x0 ∈ A.

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

An exact proof term for the current goal is HyA.

We prove the intermediate claim Hx0preA: x0 ∈ preA.

An exact proof term for the current goal is (SepI X (λz : set ⇒ apply_fun p z ∈ A) x0 Hx0X Hypx0A).

We prove the intermediate claim Hx0U: x0 ∈ U.

An exact proof term for the current goal is (HpreAsub x0 Hx0preA).

We prove the intermediate claim Hx0NotU: x0 ∉ U.

An exact proof term for the current goal is (setminusE2 X U x0 Hx0XU).

An exact proof term for the current goal is (Hx0NotU Hx0U).

We prove the intermediate claim HBsubVY: B ⊆ VY.

Let y be given.

Assume HyB: y ∈ B.

We will prove y ∈ VY.

We prove the intermediate claim HyY: y ∈ Y.

An exact proof term for the current goal is (HBsubY y HyB).

Apply (setminusI Y (image_of p (X ∖ V)) y HyY) to the current goal.

Assume HyImg: y ∈ image_of p (X ∖ V).

Apply (ReplE_impred (X ∖ V) (λx0 : set ⇒ apply_fun p x0) y HyImg) to the current goal.

Let x0 be given.

Assume Hx0XV: x0 ∈ (X ∖ V).

Assume Hypx0: y = apply_fun p x0.

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (setminusE1 X V x0 Hx0XV).

We prove the intermediate claim Hypx0B: apply_fun p x0 ∈ B.

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

An exact proof term for the current goal is HyB.

We prove the intermediate claim Hx0preB: x0 ∈ preB.

An exact proof term for the current goal is (SepI X (λz : set ⇒ apply_fun p z ∈ B) x0 Hx0X Hypx0B).

We prove the intermediate claim Hx0V: x0 ∈ V.

An exact proof term for the current goal is (HpreBsub x0 Hx0preB).

We prove the intermediate claim Hx0NotV: x0 ∉ V.

An exact proof term for the current goal is (setminusE2 X V x0 Hx0XV).

An exact proof term for the current goal is (Hx0NotV Hx0V).

We prove the intermediate claim HUVYdisj: UY ∩ VY = Empty.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ UY ∩ VY.

We will prove y ∈ Empty.

We prove the intermediate claim HyUY: y ∈ UY.

An exact proof term for the current goal is (binintersectE1 UY VY y Hy).

We prove the intermediate claim HyVY: y ∈ VY.

An exact proof term for the current goal is (binintersectE2 UY VY y Hy).

We prove the intermediate claim HyY: y ∈ Y.

An exact proof term for the current goal is (setminusE1 Y (image_of p (X ∖ U)) y HyUY).

We prove the intermediate claim HyNotImgU: y ∉ image_of p (X ∖ U).

An exact proof term for the current goal is (setminusE2 Y (image_of p (X ∖ U)) y HyUY).

We prove the intermediate claim HyNotImgV: y ∉ image_of p (X ∖ V).

An exact proof term for the current goal is (setminusE2 Y (image_of p (X ∖ V)) y HyVY).

Apply (Hsurj y HyY) to the current goal.

Let x0 be given.

Assume Hx0pair: x0 ∈ X ∧ apply_fun p x0 = y.

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (andEL (x0 ∈ X) (apply_fun p x0 = y) Hx0pair).

We prove the intermediate claim Hpx0: apply_fun p x0 = y.

An exact proof term for the current goal is (andER (x0 ∈ X) (apply_fun p x0 = y) Hx0pair).

We prove the intermediate claim Hx0U: x0 ∈ U.

Apply (xm (x0 ∈ U)) to the current goal.

An exact proof term for the current goal is (λH ⇒ H).

Assume Hx0NotU: x0 ∉ U.

We prove the intermediate claim Hx0XU: x0 ∈ (X ∖ U).

An exact proof term for the current goal is (setminusI X U x0 Hx0X Hx0NotU).

We prove the intermediate claim HyImg: y ∈ image_of p (X ∖ U).

We prove the intermediate claim Hpimg: apply_fun p x0 ∈ image_of p (X ∖ U).

An exact proof term for the current goal is (ReplI (X ∖ U) (λz : set ⇒ apply_fun p z) x0 Hx0XU).

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

An exact proof term for the current goal is Hpimg.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HyNotImgU HyImg).

We prove the intermediate claim Hx0V: x0 ∈ V.

Apply (xm (x0 ∈ V)) to the current goal.

An exact proof term for the current goal is (λH ⇒ H).

Assume Hx0NotV: x0 ∉ V.

We prove the intermediate claim Hx0XV: x0 ∈ (X ∖ V).

An exact proof term for the current goal is (setminusI X V x0 Hx0X Hx0NotV).

We prove the intermediate claim HyImg: y ∈ image_of p (X ∖ V).

We prove the intermediate claim Hpimg: apply_fun p x0 ∈ image_of p (X ∖ V).

An exact proof term for the current goal is (ReplI (X ∖ V) (λz : set ⇒ apply_fun p z) x0 Hx0XV).

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

An exact proof term for the current goal is Hpimg.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HyNotImgV HyImg).

We prove the intermediate claim Hx0UV: x0 ∈ (U ∩ V).

An exact proof term for the current goal is (binintersectI U V x0 Hx0U Hx0V).

We prove the intermediate claim HyImgUV: y ∈ image_of p (U ∩ V).

We prove the intermediate claim Hpimg: apply_fun p x0 ∈ image_of p (U ∩ V).

An exact proof term for the current goal is (ReplI (U ∩ V) (λz : set ⇒ apply_fun p z) x0 Hx0UV).

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

An exact proof term for the current goal is Hpimg.

We prove the intermediate claim HyImgEmpty: y ∈ image_of p Empty.

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

An exact proof term for the current goal is HyImgUV.

We prove the intermediate claim HyE: y ∈ Empty.

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

An exact proof term for the current goal is HyImgEmpty.

An exact proof term for the current goal is HyE.

Let y be given.

Assume Hy: y ∈ Empty.

We will prove y ∈ UY ∩ VY.

Apply FalseE to the current goal.

An exact proof term for the current goal is ((EmptyE y) Hy).

We use UY to witness the existential quantifier.

We use VY to witness the existential quantifier.

We will prove UY ∈ Ty ∧ VY ∈ Ty ∧ A ⊆ UY ∧ B ⊆ VY ∧ UY ∩ VY = Empty.

Apply and5I to the current goal.

An exact proof term for the current goal is HUYopen.

An exact proof term for the current goal is HVYopen.

An exact proof term for the current goal is HAsubUY.

An exact proof term for the current goal is HBsubVY.

An exact proof term for the current goal is HUVYdisj.