Let X, Tx, Y, Ty and f be given.
Assume Hsc: second_countable_space X Tx.
Assume Hcont: continuous_map X Tx Y Ty f.
Assume Hop: open_map X Tx Y Ty f.
Set Im to be the term image_of f X.
Set TIm to be the term subspace_topology Y Ty Im.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hsc).
We prove the intermediate claim HexB: ∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hsc).
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 Hfun: 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 Hfun (Subq_ref X)).
We prove the intermediate claim HTIm: topology_on Im TIm.
An exact proof term for the current goal is (subspace_topology_is_topology Y Ty Im HTy HImsubY).
We will prove second_countable_space Im TIm.
We will prove topology_on Im TIm ∧ ∃B : set, basis_on Im B ∧ countable_set B ∧ basis_generates Im B TIm.
Apply andI to the current goal.
An exact proof term for the current goal is HTIm.
Apply HexB to the current goal.
Let Bx be given.
Assume HBxAll: basis_on X Bx ∧ countable_set Bx ∧ basis_generates X Bx Tx.
We prove the intermediate claim HBxMid: (basis_on X Bx ∧ countable_set Bx) ∧ basis_generates X Bx Tx.
An exact proof term for the current goal is HBxAll.
We prove the intermediate claim HBxPair: basis_on X Bx ∧ countable_set Bx.
An exact proof term for the current goal is (andEL (basis_on X Bx ∧ countable_set Bx) (basis_generates X Bx Tx) HBxMid).
We prove the intermediate claim HBxBasis: basis_on X Bx.
An exact proof term for the current goal is (andEL (basis_on X Bx) (countable_set Bx) HBxPair).
We prove the intermediate claim HBxCount: countable_set Bx.
An exact proof term for the current goal is (andER (basis_on X Bx) (countable_set Bx) HBxPair).
We prove the intermediate claim HBxGener: basis_generates X Bx Tx.
An exact proof term for the current goal is (andER (basis_on X Bx ∧ countable_set Bx) (basis_generates X Bx Tx) HBxMid).
We prove the intermediate claim HTxEq: generated_topology X Bx = Tx.
An exact proof term for the current goal is (andER (basis_on X Bx) (generated_topology X Bx = Tx) HBxGener).
Set F to be the term λb : set ⇒ image_of f b ∩ Im of type set → set.
Set C to be the term {F b|b ∈ Bx}.
We prove the intermediate claim HCcount: countable_set C.
An exact proof term for the current goal is (countable_image Bx HBxCount F).
We prove the intermediate claim HopImg: ∀U : set, U ∈ Tx → image_of f U ∈ Ty.
Apply (and4E (topology_on X Tx) (topology_on Y Ty) (function_on f X Y) (∀U : set, U ∈ Tx → image_of f U ∈ Ty) Hop (∀U : set, U ∈ Tx → image_of f U ∈ Ty)) to the current goal.
Assume _ _ _ Himg.
An exact proof term for the current goal is Himg.
We prove the intermediate claim HCsub: ∀c ∈ C, c ∈ TIm.
Let c be given.
Assume HcC: c ∈ C.
Apply (ReplE_impred Bx F c HcC) to the current goal.
Let b be given.
Assume HbBx: b ∈ Bx.
Assume Hceq: c = F b.
We will prove c ∈ TIm.
rewrite the current goal using Hceq (from left to right).
We prove the intermediate claim HbGen: b ∈ generated_topology X Bx.
An exact proof term for the current goal is (generated_topology_contains_basis X Bx HBxBasis b HbBx).
We prove the intermediate claim HbTx: b ∈ Tx.
We will prove b ∈ Tx.
rewrite the current goal using HTxEq (from right to left).
An exact proof term for the current goal is HbGen.
We prove the intermediate claim HimgbTy: image_of f b ∈ Ty.
An exact proof term for the current goal is (HopImg b HbTx).
An exact proof term for the current goal is (subspace_topologyI Y Ty Im (image_of f b) HimgbTy).
We prove the intermediate claim HCref: ∀U ∈ TIm, ∀y ∈ U, ∃Cx ∈ C, y ∈ Cx ∧ Cx ⊆ U.
Let U be given.
Assume HU: U ∈ TIm.
Let y be given.
Assume HyU: y ∈ 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.
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 HUDef: U = V ∩ Im.
An exact proof term for the current goal is (andER (V ∈ Ty) (U = V ∩ Im) HVpair).
We prove the intermediate claim HyCap: y ∈ V ∩ Im.
We will prove y ∈ V ∩ Im.
rewrite the current goal using HUDef (from right to left).
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 HyCap).
We prove the intermediate claim HyIm: y ∈ Im.
An exact proof term for the current goal is (binintersectE2 V Im y HyCap).
Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) y HyIm) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume HyEq: y = apply_fun f x0.
Set W to be the term preimage_of X f V.
We prove the intermediate claim HWDef: W = preimage_of X f V.
Use reflexivity.
We prove the intermediate claim Hfx0V: apply_fun f x0 ∈ V.
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is HyV.
We prove the intermediate claim Hx0W: x0 ∈ W.
rewrite the current goal using HWDef (from left to right).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ V) x0 Hx0X Hfx0V).
We prove the intermediate claim HWTx: W ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hcont V HVTy).
We prove the intermediate claim HWGen: W ∈ generated_topology X Bx.
We will prove W ∈ generated_topology X Bx.
rewrite the current goal using HTxEq (from left to right).
An exact proof term for the current goal is HWTx.
We prove the intermediate claim HWprop: ∀x1 ∈ W, ∃b ∈ Bx, x1 ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x1 ∈ U0, ∃b ∈ Bx, x1 ∈ b ∧ b ⊆ U0) W HWGen).
We prove the intermediate claim Hexb: ∃b ∈ Bx, x0 ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (HWprop x0 Hx0W).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbBx: b ∈ Bx.
An exact proof term for the current goal is (andEL (b ∈ Bx) (x0 ∈ b ∧ b ⊆ W) Hbpair).
We prove the intermediate claim Hbprop: x0 ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (andER (b ∈ Bx) (x0 ∈ b ∧ b ⊆ W) Hbpair).
We prove the intermediate claim Hx0b: x0 ∈ b.
An exact proof term for the current goal is (andEL (x0 ∈ b) (b ⊆ W) Hbprop).
We prove the intermediate claim HbsubW: b ⊆ W.
An exact proof term for the current goal is (andER (x0 ∈ b) (b ⊆ W) Hbprop).
Set Cx to be the term F b.
We use Cx to witness the existential quantifier.
Apply andI to the current goal.
We will prove Cx ∈ C.
An exact proof term for the current goal is (ReplI Bx F b HbBx).
Apply andI to the current goal.
We will prove y ∈ Cx.
We will prove y ∈ image_of f b ∩ Im.
Apply binintersectI (image_of f b) Im y to the current goal.
We will prove 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 (λu : set ⇒ apply_fun f u) x0 Hx0b).
An exact proof term for the current goal is HyIm.
We will prove Cx ⊆ U.
rewrite the current goal using HUDef (from left to right).
We will prove Cx ⊆ V ∩ Im.
Let z be given.
Assume Hz: z ∈ Cx.
We will prove z ∈ V ∩ Im.
We prove the intermediate claim HzImg: z ∈ image_of f b.
An exact proof term for the current goal is (binintersectE1 (image_of f b) Im z Hz).
We prove the intermediate claim HzIm: z ∈ Im.
An exact proof term for the current goal is (binintersectE2 (image_of f b) Im z Hz).
We prove the intermediate claim HimgsubV: image_of f b ⊆ V.
Let z0 be given.
Assume Hz0: z0 ∈ image_of f b.
We will prove z0 ∈ V.
Apply (ReplE_impred b (λu : set ⇒ apply_fun f u) z0 Hz0) to the current goal.
Let x1 be given.
Assume Hx1b: x1 ∈ b.
Assume Hz0eq: z0 = apply_fun f x1.
We prove the intermediate claim Hx1W: x1 ∈ W.
An exact proof term for the current goal is (HbsubW 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 Hx1W).
rewrite the current goal using Hz0eq (from left to right).
An exact proof term for the current goal is Hfx1V.
Apply binintersectI V Im z to the current goal.
An exact proof term for the current goal is (HimgsubV z HzImg).
An exact proof term for the current goal is HzIm.
We prove the intermediate claim HCBasisEq: basis_on Im C ∧ generated_topology Im C = TIm.
An exact proof term for the current goal is (basis_refines_topology Im TIm C HTIm HCsub HCref).
We prove the intermediate claim HCBasis: basis_on Im C.
An exact proof term for the current goal is (andEL (basis_on Im C) (generated_topology Im C = TIm) HCBasisEq).
We prove the intermediate claim HCEq: generated_topology Im C = TIm.
An exact proof term for the current goal is (andER (basis_on Im C) (generated_topology Im C = TIm) HCBasisEq).
We use C to witness the existential quantifier.
We will prove basis_on Im C ∧ countable_set C ∧ basis_generates Im C TIm.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HCBasis.
An exact proof term for the current goal is HCcount.
We will prove basis_generates Im C TIm.
We will prove basis_on Im C ∧ generated_topology Im C = TIm.
Apply andI to the current goal.
An exact proof term for the current goal is HCBasis.
An exact proof term for the current goal is HCEq.
∎