Let X, Tx, Y, Ty and f be given.
Assume HexD: ∃D : set, D ⊆ X ∧ countable D ∧ dense_in D X Tx.
Assume Hcont: continuous_map X Tx Y Ty f.
Set Im to be the term image_of f X.
Apply HexD to the current goal.
Let D be given.
Assume HD: D ⊆ X ∧ countable D ∧ dense_in D X Tx.
We prove the intermediate claim HDpair: D ⊆ X ∧ countable D.
An exact proof term for the current goal is (andEL (D ⊆ X ∧ countable D) (dense_in D X Tx) HD).
We prove the intermediate claim HDsubX: D ⊆ X.
An exact proof term for the current goal is (andEL (D ⊆ X) (countable D) HDpair).
We prove the intermediate claim HDcount: countable D.
An exact proof term for the current goal is (andER (D ⊆ X) (countable D) HDpair).
We prove the intermediate claim Hdense: dense_in D X Tx.
An exact proof term for the current goal is (andER (D ⊆ X ∧ countable D) (dense_in D X Tx) HD).
Set Df to be the term image_of f D.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (continuous_map_topology_dom X Tx Y Ty f Hcont).
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 use Df to witness the existential quantifier.
We will prove Df ⊆ Im ∧ countable Df ∧ dense_in Df Im (subspace_topology Y Ty Im).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (image_of_mono f D X HDsubX).
We will prove countable Df.
We prove the intermediate claim HDcountset: countable_set D.
An exact proof term for the current goal is HDcount.
We prove the intermediate claim HcountDf: countable_set {(λx : set ⇒ apply_fun f x) x|x ∈ D}.
An exact proof term for the current goal is (countable_image D HDcountset (λx : set ⇒ apply_fun f x)).
An exact proof term for the current goal is HcountDf.
We will prove dense_in Df Im (subspace_topology Y Ty Im).
We will prove closure_of Im (subspace_topology Y Ty Im) Df = Im.
Apply set_ext to the current goal.
An exact proof term for the current goal is (closure_in_space Im (subspace_topology Y Ty Im) Df (subspace_topology_is_topology Y Ty Im HTy HImsubY)).
Let y be given.
Assume HyIm: y ∈ Im.
We will prove y ∈ closure_of Im (subspace_topology Y Ty Im) Df.
We prove the intermediate claim HtopIm: topology_on Im (subspace_topology Y Ty Im).
An exact proof term for the current goal is (subspace_topology_is_topology Y Ty Im HTy HImsubY).
We prove the intermediate claim Hcliff: y ∈ closure_of Im (subspace_topology Y Ty Im) Df ↔ (∀V ∈ subspace_topology Y Ty Im, y ∈ V → V ∩ Df ≠ Empty).
An exact proof term for the current goal is (closure_characterization Im (subspace_topology Y Ty Im) Df y HtopIm HyIm).
We prove the intermediate claim Hneigh: ∀V ∈ subspace_topology Y Ty Im, y ∈ V → V ∩ Df ≠ Empty.
Let V be given.
Assume HV: V ∈ subspace_topology Y Ty Im.
Assume HyV: y ∈ V.
We will prove V ∩ Df ≠ Empty.
We prove the intermediate claim HexO: ∃O ∈ Ty, V = O ∩ Im.
An exact proof term for the current goal is (subspace_topologyE Y Ty Im V HV).
Apply HexO to the current goal.
Let O be given.
Assume HOpair: O ∈ Ty ∧ V = O ∩ Im.
We prove the intermediate claim HOTy: O ∈ Ty.
An exact proof term for the current goal is (andEL (O ∈ Ty) (V = O ∩ Im) HOpair).
We prove the intermediate claim HVe: V = O ∩ Im.
An exact proof term for the current goal is (andER (O ∈ Ty) (V = O ∩ Im) HOpair).
We prove the intermediate claim HyOIm: y ∈ O ∩ Im.
We prove the intermediate claim HsubstMem: ∀S T : set, S = T → y ∈ S → y ∈ T.
Let S and T be given.
Assume HeqST: S = T.
Assume HyS: y ∈ S.
We will prove y ∈ 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 V (O ∩ Im) HVe HyV).
We prove the intermediate claim HyO: y ∈ O.
An exact proof term for the current goal is (binintersectE1 O Im y HyOIm).
Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) y HyIm (V ∩ Df ≠ Empty)) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
Assume Hyfx: y = apply_fun f x.
We prove the intermediate claim HfO: apply_fun f x ∈ O.
We prove the intermediate claim HsubstEq2: ∀S T : set, S = T → S ∈ O → T ∈ O.
Let S and T be given.
Assume HeqST: S = T.
Assume HS: S ∈ O.
We will prove T ∈ O.
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 (HsubstEq2 y (apply_fun f x) Hyfx HyO).
Set Upre to be the term preimage_of X f O.
We prove the intermediate claim HUpreTx: Upre ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hcont O HOTy).
We prove the intermediate claim HxUpre: x ∈ Upre.
We will prove x ∈ {x0 ∈ X|apply_fun f x0 ∈ O}.
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 HfO.
We prove the intermediate claim HUprene: Upre ≠ Empty.
Assume HUpreE: Upre = Empty.
Apply (EmptyE x) to the current goal.
rewrite the current goal using HUpreE (from right to left) at position 1.
An exact proof term for the current goal is HxUpre.
We prove the intermediate claim HUpreMeet: Upre ∩ D ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open D X Tx Upre HTx Hdense HUpreTx HUprene).
We prove the intermediate claim Hexd: ∃d : set, d ∈ Upre ∩ D.
An exact proof term for the current goal is (nonempty_has_element (Upre ∩ D) HUpreMeet).
Apply Hexd to the current goal.
Let d be given.
Assume HdUD: d ∈ Upre ∩ D.
We prove the intermediate claim HdUpre: d ∈ Upre.
An exact proof term for the current goal is (binintersectE1 Upre D d HdUD).
We prove the intermediate claim HdD: d ∈ D.
An exact proof term for the current goal is (binintersectE2 Upre D d HdUD).
We prove the intermediate claim HdX: d ∈ X.
An exact proof term for the current goal is (HDsubX d HdD).
We prove the intermediate claim HfdO: apply_fun f d ∈ O.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ O) d HdUpre).
We prove the intermediate claim HfdIm: apply_fun f d ∈ Im.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ apply_fun f x0) d HdX).
We prove the intermediate claim HfdV: apply_fun f d ∈ V.
We will prove apply_fun f d ∈ V.
We prove the intermediate claim HfdOIm: apply_fun f d ∈ O ∩ Im.
An exact proof term for the current goal is (binintersectI O Im (apply_fun f d) HfdO HfdIm).
We prove the intermediate claim HsubstMem2: ∀S T : set, S = T → apply_fun f d ∈ T → apply_fun f d ∈ S.
Let S and T be given.
Assume HeqST: S = T.
Assume HT: apply_fun f d ∈ T.
We will prove apply_fun f d ∈ S.
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 (HsubstMem2 V (O ∩ Im) HVe HfdOIm).
We prove the intermediate claim HfdDf: apply_fun f d ∈ Df.
An exact proof term for the current goal is (ReplI D (λx0 : set ⇒ apply_fun f x0) d HdD).
We prove the intermediate claim HfdVDf: apply_fun f d ∈ V ∩ Df.
An exact proof term for the current goal is (binintersectI V Df (apply_fun f d) HfdV HfdDf).
Assume HVE: V ∩ Df = Empty.
We prove the intermediate claim Hcontra: apply_fun f d ∈ Empty.
rewrite the current goal using HVE (from right to left).
An exact proof term for the current goal is HfdVDf.
An exact proof term for the current goal is ((EmptyE (apply_fun f d)) Hcontra).
An exact proof term for the current goal is (iffER (y ∈ closure_of Im (subspace_topology Y Ty Im) Df) (∀V ∈ subspace_topology Y Ty Im, y ∈ V → V ∩ Df ≠ Empty) Hcliff Hneigh).
∎