Let X, Tx, Y, Ty, f, A and x be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume Hcont: continuous_map X Tx Y Ty f.
Assume HAsub: A ⊆ X.
Assume Hxcl: x ∈ closure_of X Tx A.
Set fx to be the term apply_fun f x.
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 HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x Hxcl).
We prove the intermediate claim HfxY: fx ∈ Y.
An exact proof term for the current goal is (Hfun x HxX).
We will prove fx ∈ closure_of Y Ty (Repl A (λa : set ⇒ apply_fun f a)).
We prove the intermediate claim HdefCl: closure_of Y Ty (Repl A (λa : set ⇒ apply_fun f a)) = {y0 ∈ Y|∀V : set, V ∈ Ty → y0 ∈ V → V ∩ (Repl A (λa : set ⇒ apply_fun f a)) ≠ Empty}.
Use reflexivity.
rewrite the current goal using HdefCl (from left to right).
Apply (SepI Y (λy0 : set ⇒ ∀V : set, V ∈ Ty → y0 ∈ V → V ∩ (Repl A (λa : set ⇒ apply_fun f a)) ≠ Empty) fx HfxY) to the current goal.
Let V be given.
Assume HV: V ∈ Ty.
Assume HfxV: fx ∈ V.
We will prove V ∩ (Repl A (λa : set ⇒ apply_fun f a)) ≠ Empty.
We prove the intermediate claim Hpre: 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).
We prove the intermediate claim Hxpre: x ∈ preimage_of X f V.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ V) x HxX HfxV).
We prove the intermediate claim Hclx: ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x Hxcl).
We prove the intermediate claim Hmeet: (preimage_of X f V) ∩ A ≠ Empty.
An exact proof term for the current goal is (Hclx (preimage_of X f V) Hpre Hxpre).
We prove the intermediate claim Hexa: ∃a : set, a ∈ (preimage_of X f V) ∩ A.
An exact proof term for the current goal is (nonempty_has_element ((preimage_of X f V) ∩ A) Hmeet).
Apply Hexa to the current goal.
Let a be given.
Assume Ha: a ∈ (preimage_of X f V) ∩ A.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (binintersectE2 (preimage_of X f V) A a Ha).
We prove the intermediate claim HafV: apply_fun f a ∈ V.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ V) a (binintersectE1 (preimage_of X f V) A a Ha)).
Set y to be the term apply_fun f a.
We prove the intermediate claim HyImg: y ∈ Repl A (λa0 : set ⇒ apply_fun f a0).
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ apply_fun f a0) a HaA).
We prove the intermediate claim HyIn: y ∈ V ∩ (Repl A (λa0 : set ⇒ apply_fun f a0)).
An exact proof term for the current goal is (binintersectI V (Repl A (λa0 : set ⇒ apply_fun f a0)) y HafV HyImg).
An exact proof term for the current goal is (elem_implies_nonempty (V ∩ (Repl A (λa0 : set ⇒ apply_fun f a0))) y HyIn).
∎