Let V be given.

Assume HV: V ∈ Ty.

We will prove preimage_of (function_space X Y) eval V ∈ (pointwise_convergence_topology X Tx Y Ty).

Set S0 to be the term {f ∈ function_space X Y|apply_fun f x ∈ V}.

We prove the intermediate claim HS0inSub: S0 ∈ pointwise_subbasis X Tx Y Ty.

We prove the intermediate claim HS0sub: S0 ⊆ function_space X Y.

Let f be given.

Assume HfS0: f ∈ S0.

An exact proof term for the current goal is (SepE1 (function_space X Y) (λf0 : set ⇒ apply_fun f0 x ∈ V) f HfS0).

We prove the intermediate claim HS0pow: S0 ∈ 𝒫 (function_space X Y).

An exact proof term for the current goal is (PowerI (function_space X Y) S0 HS0sub).

We prove the intermediate claim HS0prop: ∃x0 U : set, x0 ∈ X ∧ U ∈ Ty ∧ S0 = {f0 ∈ function_space X Y|apply_fun f0 x0 ∈ U}.

We use x to witness the existential quantifier.

We use V to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is HV.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 (function_space X Y)) (λS : set ⇒ ∃x0 U : set, x0 ∈ X ∧ U ∈ Ty ∧ S = {f0 ∈ function_space X Y|apply_fun f0 x0 ∈ U}) S0 HS0pow HS0prop).

We prove the intermediate claim HpreEq: preimage_of (function_space X Y) eval V = S0.

Apply set_ext to the current goal.

Let f be given.

Assume Hfpre: f ∈ preimage_of (function_space X Y) eval V.

We will prove f ∈ S0.

We prove the intermediate claim HfDom: f ∈ function_space X Y.

An exact proof term for the current goal is (SepE1 (function_space X Y) (λu : set ⇒ apply_fun eval u ∈ V) f Hfpre).

We prove the intermediate claim HevalV: apply_fun eval f ∈ V.

An exact proof term for the current goal is (SepE2 (function_space X Y) (λu : set ⇒ apply_fun eval u ∈ V) f Hfpre).

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

rewrite the current goal using (apply_fun_graph (function_space X Y) (λg : set ⇒ apply_fun g x) f HfDom) (from right to left).

An exact proof term for the current goal is HevalV.

An exact proof term for the current goal is (SepI (function_space X Y) (λf0 : set ⇒ apply_fun f0 x ∈ V) f HfDom HfxV).

Let f be given.

Assume HfS0: f ∈ S0.

We will prove f ∈ preimage_of (function_space X Y) eval V.

We prove the intermediate claim HfDom: f ∈ function_space X Y.

An exact proof term for the current goal is (SepE1 (function_space X Y) (λf0 : set ⇒ apply_fun f0 x ∈ V) f HfS0).

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

An exact proof term for the current goal is (SepE2 (function_space X Y) (λf0 : set ⇒ apply_fun f0 x ∈ V) f HfS0).

We prove the intermediate claim HevalV: apply_fun eval f ∈ V.

rewrite the current goal using (apply_fun_graph (function_space X Y) (λg : set ⇒ apply_fun g x) f HfDom) (from left to right).

An exact proof term for the current goal is HfxV.

An exact proof term for the current goal is (SepI (function_space X Y) (λu : set ⇒ apply_fun eval u ∈ V) f HfDom HevalV).

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

Set S to be the term (pointwise_subbasis X Tx Y Ty) ∪ {function_space X Y}.

We prove the intermediate claim HS: subbasis_on (function_space X Y) S.

We will prove S ⊆ 𝒫 (function_space X Y) ∧ ⋃ S = function_space X Y.

Apply andI to the current goal.

Let s be given.

Assume Hs: s ∈ S.

We will prove s ∈ 𝒫 (function_space X Y).

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {function_space X Y} s (s ∈ 𝒫 (function_space X Y))) to the current goal.

Assume Hsp: s ∈ pointwise_subbasis X Tx Y Ty.

An exact proof term for the current goal is (SepE1 (𝒫 (function_space X Y)) (λS0 : set ⇒ ∃x0 U : set, x0 ∈ X ∧ U ∈ Ty ∧ S0 = {f0 ∈ function_space X Y|apply_fun f0 x0 ∈ U}) s Hsp).

Assume HsDom: s ∈ {function_space X Y}.

We prove the intermediate claim Hseq: s = function_space X Y.

An exact proof term for the current goal is (SingE (function_space X Y) s HsDom).

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

An exact proof term for the current goal is (PowerI (function_space X Y) (function_space X Y) (Subq_ref (function_space X Y))).

An exact proof term for the current goal is Hs.

Apply set_ext to the current goal.

Let f be given.

Assume Hf: f ∈ ⋃ S.

Apply (UnionE_impred S f Hf (f ∈ function_space X Y)) to the current goal.

Let U be given.

Assume HfU: f ∈ U.

Assume HU: U ∈ S.

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {function_space X Y} U (f ∈ function_space X Y)) to the current goal.

Assume HUp: U ∈ pointwise_subbasis X Tx Y Ty.

We prove the intermediate claim HUpow: U ∈ 𝒫 (function_space X Y).

An exact proof term for the current goal is (SepE1 (𝒫 (function_space X Y)) (λS0 : set ⇒ ∃x0 U0 : set, x0 ∈ X ∧ U0 ∈ Ty ∧ S0 = {f0 ∈ function_space X Y|apply_fun f0 x0 ∈ U0}) U HUp).

An exact proof term for the current goal is (PowerE (function_space X Y) U HUpow f HfU).

Assume HUDom: U ∈ {function_space X Y}.

We prove the intermediate claim HUeq: U = function_space X Y.

An exact proof term for the current goal is (SingE (function_space X Y) U HUDom).

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

An exact proof term for the current goal is HfU.

An exact proof term for the current goal is HU.

Let f be given.

Assume Hf: f ∈ function_space X Y.

We prove the intermediate claim HDomInS: function_space X Y ∈ S.

An exact proof term for the current goal is (binunionI2 (pointwise_subbasis X Tx Y Ty) {function_space X Y} (function_space X Y) (SingI (function_space X Y))).

An exact proof term for the current goal is (UnionI S f (function_space X Y) Hf HDomInS).

We prove the intermediate claim HS0inS: S0 ∈ S.

An exact proof term for the current goal is (binunionI1 (pointwise_subbasis X Tx Y Ty) {function_space X Y} S0 HS0inSub).

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis (function_space X Y) S S0 HS HS0inS).