Let U be given.

Assume HcoverIm: open_cover Im (subspace_topology Y Ty Im) U.

We will prove ∃V : set, countable_subcollection V U ∧ covers Im V.

We prove the intermediate claim HUmem: ∀u : set, u ∈ U → u ∈ subspace_topology Y Ty Im.

An exact proof term for the current goal is (andEL (∀u : set, u ∈ U → u ∈ subspace_topology Y Ty Im) (covers Im U) HcoverIm).

We prove the intermediate claim HUcov: covers Im U.

An exact proof term for the current goal is (andER (∀u : set, u ∈ U → u ∈ subspace_topology Y Ty Im) (covers Im U) HcoverIm).

Set Wfam to be the term {V ∈ Ty|V ∩ Im ∈ U}.

Set P to be the term {preimage_of X f V|V ∈ Wfam}.

We prove the intermediate claim HPcover: open_cover X Tx P.

We will prove (∀p : set, p ∈ P → p ∈ Tx) ∧ covers X P.

Apply andI to the current goal.

Let p be given.

Assume Hp: p ∈ P.

We will prove p ∈ Tx.

Apply (ReplE_impred Wfam (λV0 : set ⇒ preimage_of X f V0) p Hp (p ∈ Tx)) to the current goal.

Let V0 be given.

Assume HV0W: V0 ∈ Wfam.

Assume Hpeq: p = preimage_of X f V0.

We prove the intermediate claim HV0Ty: V0 ∈ Ty.

An exact proof term for the current goal is (SepE1 Ty (λV1 : set ⇒ V1 ∩ Im ∈ U) V0 HV0W).

We prove the intermediate claim Hpre: preimage_of X f V0 ∈ Tx.

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

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

An exact proof term for the current goal is Hpre.

We will prove covers X P.

Let x be given.

Assume HxX: x ∈ X.

We will prove ∃p : set, p ∈ P ∧ x ∈ p.

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 Hexu: ∃u : set, u ∈ U ∧ apply_fun f x ∈ u.

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

Apply Hexu to the current goal.

Let u be given.

Assume Hupair: u ∈ U ∧ apply_fun f x ∈ u.

We prove the intermediate claim HuU: u ∈ U.

An exact proof term for the current goal is (andEL (u ∈ U) (apply_fun f x ∈ u) Hupair).

We prove the intermediate claim Hfxu: apply_fun f x ∈ u.

An exact proof term for the current goal is (andER (u ∈ U) (apply_fun f x ∈ u) Hupair).

We prove the intermediate claim HuSub: u ∈ subspace_topology Y Ty Im.

An exact proof term for the current goal is (HUmem u HuU).

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 HuSub).

Apply HexV to the current goal.

Let V be given.

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

We prove the intermediate claim HVTy: 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 HfxVIm: apply_fun f x ∈ V ∩ Im.

We prove the intermediate claim HsubstMem: ∀S T : set, S = T → apply_fun f x ∈ S → apply_fun f x ∈ T.

Let S and T be given.

Assume HeqST: S = T.

Assume HyS: apply_fun f x ∈ S.

We will prove apply_fun f x ∈ T.

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

An exact proof term for the current goal is HyS.

An exact proof term for the current goal is (HsubstMem u (V ∩ Im) Hueq Hfxu).

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

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

We prove the intermediate claim HxPre: x ∈ preimage_of X f V.

We will prove x ∈ {x0 ∈ X|apply_fun f x0 ∈ V}.

Apply SepI to the current goal.

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is HfxV.

We prove the intermediate claim HVWfam: V ∈ Wfam.

Apply SepI to the current goal.

An exact proof term for the current goal is HVTy.

We prove the intermediate claim HsubstU: ∀S T : set, S = T → S ∈ U → T ∈ U.

Let S and T be given.

Assume HeqST: S = T.

Assume HS: S ∈ U.

We will prove T ∈ U.

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

An exact proof term for the current goal is HS.

An exact proof term for the current goal is (HsubstU u (V ∩ Im) Hueq HuU).

We use (preimage_of X f V) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplI Wfam (λV0 : set ⇒ preimage_of X f V0) V HVWfam).

An exact proof term for the current goal is HxPre.

We prove the intermediate claim HexP0: ∃P0 : set, countable_subcollection P0 P ∧ covers X P0.

An exact proof term for the current goal is (HLXprop P HPcover).

Apply HexP0 to the current goal.

Let P0 be given.

Assume HP0: countable_subcollection P0 P ∧ covers X P0.

We prove the intermediate claim HP0subcoll: countable_subcollection P0 P.

An exact proof term for the current goal is (andEL (countable_subcollection P0 P) (covers X P0) HP0).

We prove the intermediate claim HP0covers: covers X P0.

An exact proof term for the current goal is (andER (countable_subcollection P0 P) (covers X P0) HP0).

We prove the intermediate claim HP0sub: P0 ⊆ P.

An exact proof term for the current goal is (andEL (P0 ⊆ P) (countable_set P0) HP0subcoll).

We prove the intermediate claim HP0count: countable_set P0.

An exact proof term for the current goal is (andER (P0 ⊆ P) (countable_set P0) HP0subcoll).

Set preV to be the term (λp : set ⇒ Eps_i (λV : set ⇒ V ∈ Wfam ∧ p = preimage_of X f V)).

Set W0 to be the term {preV p|p ∈ P0}.

We prove the intermediate claim HW0count: countable_set W0.

An exact proof term for the current goal is (countable_image P0 HP0count preV).

Set V to be the term {(W ∩ Im)|W ∈ W0}.

We use V to witness the existential quantifier.

We will prove countable_subcollection V U ∧ covers Im V.

Apply andI to the current goal.

We will prove countable_subcollection V U.

We will prove V ⊆ U ∧ countable_set V.

Apply andI to the current goal.

We will prove V ⊆ U.

Let u be given.

Assume Hu: u ∈ V.

We will prove u ∈ U.

Apply (ReplE_impred W0 (λW : set ⇒ W ∩ Im) u Hu (u ∈ U)) to the current goal.

Let W be given.

Assume HW0: W ∈ W0.

Assume Hueq: u = W ∩ Im.

Apply (ReplE_impred P0 preV W HW0 (u ∈ U)) to the current goal.

Let p be given.

Assume Hp0: p ∈ P0.

Assume HWdef: W = preV p.

We prove the intermediate claim Hueq2: u = preV p ∩ Im.

We will prove u = preV p ∩ Im.

We prove the intermediate claim Hrhs: W ∩ Im = preV p ∩ Im.

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

Use reflexivity.

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

An exact proof term for the current goal is Hueq.

We prove the intermediate claim HpP: p ∈ P.

An exact proof term for the current goal is (HP0sub p Hp0).

We prove the intermediate claim HexWV: ∃V0 : set, V0 ∈ Wfam ∧ p = preimage_of X f V0.

Apply (ReplE_impred Wfam (λV0 : set ⇒ preimage_of X f V0) p HpP (∃V0 : set, V0 ∈ Wfam ∧ p = preimage_of X f V0)) to the current goal.

Let V0 be given.

Assume HV0W: V0 ∈ Wfam.

Assume Hpeq: p = preimage_of X f V0.

We use V0 to witness the existential quantifier.

An exact proof term for the current goal is (andI (V0 ∈ Wfam) (p = preimage_of X f V0) HV0W Hpeq).

We prove the intermediate claim HpreVprop: preV p ∈ Wfam ∧ p = preimage_of X f (preV p).

An exact proof term for the current goal is (Eps_i_ex (λV0 : set ⇒ V0 ∈ Wfam ∧ p = preimage_of X f V0) HexWV).

We prove the intermediate claim HWfam: preV p ∈ Wfam.

An exact proof term for the current goal is (andEL (preV p ∈ Wfam) (p = preimage_of X f (preV p)) HpreVprop).

We prove the intermediate claim HWinU: preV p ∩ Im ∈ U.

An exact proof term for the current goal is (SepE2 Ty (λV0 : set ⇒ V0 ∩ Im ∈ U) (preV p) HWfam).

We prove the intermediate claim HsubstEq: ∀S T : set, S = T → T ∈ U → S ∈ U.

Let S and T be given.

Assume HeqST: S = T.

Assume HTU: T ∈ U.

We will prove S ∈ U.

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

An exact proof term for the current goal is HTU.

An exact proof term for the current goal is (HsubstEq u (preV p ∩ Im) Hueq2 HWinU).

We prove the intermediate claim HW0count2: countable_set W0.

An exact proof term for the current goal is HW0count.

An exact proof term for the current goal is (countable_image W0 HW0count2 (λW : set ⇒ W ∩ Im)).

We will prove covers Im V.

Let y be given.

Assume HyIm: y ∈ Im.

We will prove ∃u : set, u ∈ V ∧ y ∈ u.

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

Let x be given.

Assume HxX: x ∈ X.

Assume Hyfx: y = apply_fun f x.

We prove the intermediate claim Hexp: ∃p : set, p ∈ P0 ∧ x ∈ p.

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

Apply Hexp to the current goal.

Let p be given.

Assume Hppair: p ∈ P0 ∧ x ∈ p.

We prove the intermediate claim Hp0: p ∈ P0.

An exact proof term for the current goal is (andEL (p ∈ P0) (x ∈ p) Hppair).

We prove the intermediate claim Hxp: x ∈ p.

An exact proof term for the current goal is (andER (p ∈ P0) (x ∈ p) Hppair).

We prove the intermediate claim HpP: p ∈ P.

An exact proof term for the current goal is (HP0sub p Hp0).

We prove the intermediate claim HexWV: ∃V0 : set, V0 ∈ Wfam ∧ p = preimage_of X f V0.

Apply (ReplE_impred Wfam (λV0 : set ⇒ preimage_of X f V0) p HpP (∃V0 : set, V0 ∈ Wfam ∧ p = preimage_of X f V0)) to the current goal.

Let V0 be given.

Assume HV0W: V0 ∈ Wfam.

Assume Hpeq: p = preimage_of X f V0.

We use V0 to witness the existential quantifier.

An exact proof term for the current goal is (andI (V0 ∈ Wfam) (p = preimage_of X f V0) HV0W Hpeq).

We prove the intermediate claim HpreVprop: preV p ∈ Wfam ∧ p = preimage_of X f (preV p).

An exact proof term for the current goal is (Eps_i_ex (λV0 : set ⇒ V0 ∈ Wfam ∧ p = preimage_of X f V0) HexWV).

We prove the intermediate claim Hpeq: p = preimage_of X f (preV p).

An exact proof term for the current goal is (andER (preV p ∈ Wfam) (p = preimage_of X f (preV p)) HpreVprop).

We prove the intermediate claim HxPre: x ∈ preimage_of X f (preV p).

We prove the intermediate claim HsubstMem: ∀S T : set, S = T → x ∈ S → x ∈ T.

Let S and T be given.

Assume HeqST: S = T.

Assume HxS: x ∈ S.

We will prove x ∈ T.

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

An exact proof term for the current goal is HxS.

An exact proof term for the current goal is (HsubstMem p (preimage_of X f (preV p)) Hpeq Hxp).

We prove the intermediate claim Hfyin: apply_fun f x ∈ preV p.

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

We use (preV p ∩ Im) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplI W0 (λW : set ⇒ W ∩ Im) (preV p) (ReplI P0 preV p Hp0)).

We prove the intermediate claim HyIm2: 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 HyIn: apply_fun f x ∈ preV p ∩ Im.

An exact proof term for the current goal is (binintersectI (preV p) Im (apply_fun f x) Hfyin HyIm2).

We prove the intermediate claim HsubstEq2: ∀S T : set, S = T → T ∈ (preV p ∩ Im) → S ∈ (preV p ∩ Im).

Let S and T be given.

Assume HeqST: S = T.

Assume HT: T ∈ (preV p ∩ Im).

We will prove S ∈ (preV p ∩ Im).

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

An exact proof term for the current goal is HT.

An exact proof term for the current goal is (HsubstEq2 y (apply_fun f x) Hyfx HyIn).