Let X, Tx, Y, Ty and f be given.
Assume Hhom: homeomorphism X Tx Y Ty f.
Assume HscY: second_countable_space Y Ty.
We prove the intermediate claim Hcontf: continuous_map X Tx Y Ty f.
An exact proof term for the current goal is (homeomorphism_continuous X Tx Y Ty f Hhom).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (homeomorphism_topology_left X Tx Y Ty f Hhom).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (homeomorphism_topology_right X Tx Y Ty f Hhom).
We prove the intermediate claim Hfunf: function_on f X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y Ty f Hcontf).
We prove the intermediate claim Hexg: ∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y).
An exact proof term for the current goal is (homeomorphism_inverse_package X Tx Y Ty f Hhom).
Apply Hexg to the current goal.
Let g be given.
Assume Hgpack.
We prove the intermediate claim Hcoreg: continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x).
An exact proof term for the current goal is (andEL (continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x)) (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y) Hgpack).
We prove the intermediate claim Hcontg: continuous_map Y Ty X Tx g.
An exact proof term for the current goal is (andEL (continuous_map Y Ty X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) Hcoreg).
We prove the intermediate claim Hgf: ∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x.
An exact proof term for the current goal is (andER (continuous_map Y Ty X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) Hcoreg).
We prove the intermediate claim Hfg: ∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y.
An exact proof term for the current goal is (andER (continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x)) (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y) Hgpack).
We prove the intermediate claim HexB: ∃B : set, basis_on Y B ∧ countable_set B ∧ basis_generates Y B Ty.
An exact proof term for the current goal is (andER (topology_on Y Ty) (∃B : set, basis_on Y B ∧ countable_set B ∧ basis_generates Y B Ty) HscY).
Apply HexB to the current goal.
Let B be given.
Assume HBpack: basis_on Y B ∧ countable_set B ∧ basis_generates Y B Ty.
We prove the intermediate claim HBmid: (basis_on Y B ∧ countable_set B) ∧ basis_generates Y B Ty.
An exact proof term for the current goal is HBpack.
We prove the intermediate claim HBpair: basis_on Y B ∧ countable_set B.
An exact proof term for the current goal is (andEL (basis_on Y B ∧ countable_set B) (basis_generates Y B Ty) HBmid).
We prove the intermediate claim HBasis: basis_on Y B.
An exact proof term for the current goal is (andEL (basis_on Y B) (countable_set B) HBpair).
We prove the intermediate claim HBcount: countable_set B.
An exact proof term for the current goal is (andER (basis_on Y B) (countable_set B) HBpair).
We prove the intermediate claim HBgen: basis_generates Y B Ty.
An exact proof term for the current goal is (andER (basis_on Y B ∧ countable_set B) (basis_generates Y B Ty) HBmid).
We prove the intermediate claim HgenEq: generated_topology Y B = Ty.
An exact proof term for the current goal is (andER (basis_on Y B) (generated_topology Y B = Ty) HBgen).
Set F to be the term λb : set ⇒ preimage_of X f b of type set → set.
Set Bx to be the term {F b|b ∈ B}.
We prove the intermediate claim HBxCount: countable_set Bx.
An exact proof term for the current goal is (countable_image B HBcount F).
We prove the intermediate claim HBxSub: ∀c ∈ Bx, c ∈ Tx.
Let c be given.
Assume Hc: c ∈ Bx.
Apply (ReplE_impred B F c Hc) to the current goal.
Let b be given.
Assume HbB: b ∈ B.
Assume Hceq: c = F b.
We will prove c ∈ Tx.
rewrite the current goal using Hceq (from left to right).
We prove the intermediate claim HbsubY: b ⊆ Y.
An exact proof term for the current goal is (basis_elem_subset Y B b HBasis HbB).
We prove the intermediate claim HbPow: b ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y b HbsubY).
We prove the intermediate claim HbGen: b ∈ generated_topology Y B.
An exact proof term for the current goal is (generated_topology_contains_elem Y B b HbPow HbB).
We prove the intermediate claim HbTy: b ∈ Ty.
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HbGen.
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hcontf b HbTy).
We prove the intermediate claim HBxRef: ∀U ∈ Tx, ∀x ∈ U, ∃Cx ∈ Bx, x ∈ Cx ∧ Cx ⊆ U.
Let U be given.
Assume HU: U ∈ Tx.
Let x be given.
Assume HxU: x ∈ U.
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).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsubX x HxU).
Set Vopen to be the term preimage_of Y g U.
We prove the intermediate claim HVopenTy: Vopen ∈ Ty.
An exact proof term for the current goal is (continuous_map_preimage Y Ty X Tx g Hcontg U HU).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfunf x HxX).
We prove the intermediate claim Hfxx: apply_fun g (apply_fun f x) = x.
An exact proof term for the current goal is (Hgf x HxX).
We prove the intermediate claim HfxVopen: apply_fun f x ∈ Vopen.
We will prove apply_fun f x ∈ preimage_of Y g U.
We prove the intermediate claim HgfxU: apply_fun g (apply_fun f x) ∈ U.
rewrite the current goal using Hfxx (from left to right).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (SepI Y (λy0 : set ⇒ apply_fun g y0 ∈ U) (apply_fun f x) HfxY HgfxU).
We prove the intermediate claim HVopenGen: Vopen ∈ generated_topology Y B.
rewrite the current goal using HgenEq (from left to right).
An exact proof term for the current goal is HVopenTy.
We prove the intermediate claim Hlocal: ∃b ∈ B, apply_fun f x ∈ b ∧ b ⊆ Vopen.
An exact proof term for the current goal is (generated_topology_local_refine Y B Vopen (apply_fun f x) HVopenGen HfxVopen).
Apply Hlocal to the current goal.
Let b be given.
Assume Hbpack.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (apply_fun f x ∈ b ∧ b ⊆ Vopen) Hbpack).
We prove the intermediate claim Hbrest: apply_fun f x ∈ b ∧ b ⊆ Vopen.
An exact proof term for the current goal is (andER (b ∈ B) (apply_fun f x ∈ b ∧ b ⊆ Vopen) Hbpack).
We prove the intermediate claim Hfxb: apply_fun f x ∈ b.
An exact proof term for the current goal is (andEL (apply_fun f x ∈ b) (b ⊆ Vopen) Hbrest).
We prove the intermediate claim HbsubV: b ⊆ Vopen.
An exact proof term for the current goal is (andER (apply_fun f x ∈ b) (b ⊆ Vopen) Hbrest).
Set Cx to be the term preimage_of X f b.
We use Cx to witness the existential quantifier.
We will prove Cx ∈ Bx ∧ (x ∈ Cx ∧ Cx ⊆ U).
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI B F b HbB).
Apply andI to the current goal.
We will prove x ∈ preimage_of X f b.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ b) x HxX Hfxb).
We will prove preimage_of X f b ⊆ U.
Let z be given.
Assume Hz: z ∈ preimage_of X f b.
We will prove z ∈ U.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ b) z Hz).
We prove the intermediate claim Hfz: apply_fun f z ∈ b.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ b) z Hz).
We prove the intermediate claim HfzV: apply_fun f z ∈ Vopen.
An exact proof term for the current goal is (HbsubV (apply_fun f z) Hfz).
We prove the intermediate claim HgFzU: apply_fun g (apply_fun f z) ∈ U.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ apply_fun g y0 ∈ U) (apply_fun f z) HfzV).
rewrite the current goal using (Hgf z HzX) (from right to left).
An exact proof term for the current goal is HgFzU.
We prove the intermediate claim HBasisGen: basis_on X Bx ∧ generated_topology X Bx = Tx.
An exact proof term for the current goal is (basis_refines_topology X Tx Bx HTx HBxSub HBxRef).
We will prove second_countable_space X Tx.
We will prove topology_on X Tx ∧ ∃B0 : set, basis_on X B0 ∧ countable_set B0 ∧ basis_generates X B0 Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We use Bx to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (basis_on X Bx) (generated_topology X Bx = Tx) HBasisGen).
An exact proof term for the current goal is HBxCount.
An exact proof term for the current goal is HBasisGen.
∎