Let y be given.

Assume Hy: y ∈ Im.

We will prove countable_basis_at Im (subspace_topology Y Ty Im) y.

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

Let x0 be given.

Assume Hx0X: x0 ∈ X.

Assume Hyeq: y = apply_fun f x0.

We prove the intermediate claim Hbasis0: countable_basis_at X Tx x0.

An exact proof term for the current goal is (HX1prop x0 Hx0X).

We prove the intermediate claim HexBx: ∃Bx : set, Bx ⊆ Tx ∧ countable_set Bx ∧ (∀b : set, b ∈ Bx → x0 ∈ b) ∧ (∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U).

An exact proof term for the current goal is (andER (topology_on X Tx ∧ x0 ∈ X) (∃Bx : set, Bx ⊆ Tx ∧ countable_set Bx ∧ (∀b : set, b ∈ Bx → x0 ∈ b) ∧ (∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U)) Hbasis0).

Apply HexBx to the current goal.

Let Bx be given.

Assume HBx: Bx ⊆ Tx ∧ countable_set Bx ∧ (∀b : set, b ∈ Bx → x0 ∈ b) ∧ (∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U).

We prove the intermediate claim HBxsubTx: Bx ⊆ Tx.

Apply (and4E (Bx ⊆ Tx) (countable_set Bx) (∀b : set, b ∈ Bx → x0 ∈ b) (∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U) HBx (Bx ⊆ Tx)) to the current goal.

Assume H1 H2 H3 H4.

An exact proof term for the current goal is H1.

We prove the intermediate claim HBxcount: countable_set Bx.

Apply (and4E (Bx ⊆ Tx) (countable_set Bx) (∀b : set, b ∈ Bx → x0 ∈ b) (∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U) HBx (countable_set Bx)) to the current goal.

Assume H1 H2 H3 H4.

An exact proof term for the current goal is H2.

We prove the intermediate claim HBxmem: ∀b : set, b ∈ Bx → x0 ∈ b.

Apply (and4E (Bx ⊆ Tx) (countable_set Bx) (∀b : set, b ∈ Bx → x0 ∈ b) (∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U) HBx (∀b : set, b ∈ Bx → x0 ∈ b)) to the current goal.

Assume H1 H2 H3 H4.

An exact proof term for the current goal is H3.

We prove the intermediate claim HBxrefine: ∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U.

Apply (and4E (Bx ⊆ Tx) (countable_set Bx) (∀b : set, b ∈ Bx → x0 ∈ b) (∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U) HBx (∀U : set, U ∈ Tx → x0 ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U)) to the current goal.

Assume H1 H2 H3 H4.

An exact proof term for the current goal is H4.

Set B to be the term {image_of f b ∩ Im|b ∈ Bx}.

We will prove topology_on Im (subspace_topology Y Ty Im) ∧ y ∈ Im ∧ ∃B0 : set, B0 ⊆ subspace_topology Y Ty Im ∧ countable_set B0 ∧ (∀b0 : set, b0 ∈ B0 → y ∈ b0) ∧ (∀U : set, U ∈ subspace_topology Y Ty Im → y ∈ U → ∃b0 : set, b0 ∈ B0 ∧ b0 ⊆ U).

Apply and3I to the current goal.

An exact proof term for the current goal is HImTop.

An exact proof term for the current goal is Hy.

We use B to witness the existential quantifier.

Apply and4I to the current goal.

Let b0 be given.

Assume Hb0: b0 ∈ B.

We will prove b0 ∈ subspace_topology Y Ty Im.

Apply (ReplE_impred Bx (λb : set ⇒ image_of f b ∩ Im) b0 Hb0) to the current goal.

Let b be given.

Assume HbBx: b ∈ Bx.

Assume Hb0eq: b0 = image_of f b ∩ Im.

We prove the intermediate claim HbTx: b ∈ Tx.

An exact proof term for the current goal is (HBxsubTx b HbBx).

We prove the intermediate claim HimgOpen: ∀U : set, U ∈ Tx → image_of f U ∈ Ty.

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

We prove the intermediate claim HVTy: image_of f b ∈ Ty.

An exact proof term for the current goal is (HimgOpen b HbTx).

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

An exact proof term for the current goal is (subspace_topologyI Y Ty Im (image_of f b) HVTy).

An exact proof term for the current goal is (countable_image Bx HBxcount (λb : set ⇒ image_of f b ∩ Im)).

Let b0 be given.

Assume Hb0: b0 ∈ B.

We will prove y ∈ b0.

Apply (ReplE_impred Bx (λb : set ⇒ image_of f b ∩ Im) b0 Hb0) to the current goal.

Let b be given.

Assume HbBx: b ∈ Bx.

Assume Hb0eq: b0 = image_of f b ∩ Im.

We prove the intermediate claim Hx0b: x0 ∈ b.

An exact proof term for the current goal is (HBxmem b HbBx).

We prove the intermediate claim Hyimg: y ∈ image_of f b.

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

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

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

An exact proof term for the current goal is (binintersectI (image_of f b) Im y Hyimg Hy).

Let U be given.

Assume HU: U ∈ subspace_topology Y Ty Im.

Assume HyU: y ∈ U.

We will prove ∃b0 : set, b0 ∈ B ∧ b0 ⊆ U.

We prove the intermediate claim HexV: ∃V ∈ Ty, U = V ∩ Im.

An exact proof term for the current goal is (subspace_topologyE Y Ty Im U HU).

Apply HexV to the current goal.

Let V be given.

Assume HVpair: V ∈ Ty ∧ U = V ∩ Im.

We prove the intermediate claim HV: V ∈ Ty.

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

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

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

We prove the intermediate claim HyVIm: y ∈ V ∩ Im.

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

An exact proof term for the current goal is HyU.

We prove the intermediate claim HyV: y ∈ V.

An exact proof term for the current goal is (binintersectE1 V Im y HyVIm).

We prove the intermediate claim Hfx0V: apply_fun f x0 ∈ V.

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

An exact proof term for the current goal is HyV.

We prove the intermediate claim Hx0pre: x0 ∈ preimage_of X f V.

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

We prove the intermediate claim HpreTx: preimage_of X f V ∈ Tx.

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

Apply (HBxrefine (preimage_of X f V) HpreTx Hx0pre) to the current goal.

Let b be given.

Assume Hbpair: b ∈ Bx ∧ b ⊆ preimage_of X f V.

We prove the intermediate claim HbBx: b ∈ Bx.

An exact proof term for the current goal is (andEL (b ∈ Bx) (b ⊆ preimage_of X f V) Hbpair).

We prove the intermediate claim Hbsub: b ⊆ preimage_of X f V.

An exact proof term for the current goal is (andER (b ∈ Bx) (b ⊆ preimage_of X f V) Hbpair).

Set b0 to be the term image_of f b ∩ Im.

We use b0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplI Bx (λb1 : set ⇒ image_of f b1 ∩ Im) b HbBx).

We will prove b0 ⊆ U.

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

Apply (binintersect_Subq_max V Im b0) to the current goal.

We prove the intermediate claim Hb0subImg: b0 ⊆ image_of f b.

An exact proof term for the current goal is (binintersect_Subq_1 (image_of f b) Im).

We prove the intermediate claim HimgsubV: image_of f b ⊆ V.

Let z be given.

Assume Hz: z ∈ image_of f b.

We will prove z ∈ V.

Apply (ReplE_impred b (λx1 : set ⇒ apply_fun f x1) z Hz) to the current goal.

Let x1 be given.

Assume Hx1b: x1 ∈ b.

Assume Hzeq: z = apply_fun f x1.

We prove the intermediate claim Hx1pre: x1 ∈ preimage_of X f V.

An exact proof term for the current goal is (Hbsub x1 Hx1b).

We prove the intermediate claim Hfx1V: apply_fun f x1 ∈ V.

An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ V) x1 Hx1pre).

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

An exact proof term for the current goal is Hfx1V.

An exact proof term for the current goal is (Subq_tra b0 (image_of f b) V Hb0subImg HimgsubV).

An exact proof term for the current goal is (binintersect_Subq_2 (image_of f b) Im).