Let X, Tx, A and x be given.
Assume HTx: topology_on X Tx.
We will prove x ∈ closure_of X Tx A ↔ ∃net J le : set, net_converges_on X Tx net J le x ∧ net_points_in A net J.
Apply iffI to the current goal.
Assume Hxcl: x ∈ closure_of X Tx A.
We will prove ∃net J le : set, net_converges_on X Tx net J le x ∧ net_points_in A net J.
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 Hmeet: ∀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).
Set J to be the term {U ∈ Tx|x ∈ U}.
Set le to be the term rev_inclusion_rel J.
Set g to be the term λU : set ⇒ Eps_i (λy : set ⇒ y ∈ U ∩ A).
Set net to be the term graph J g.
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_sub_Power X Tx HTx).
We prove the intermediate claim HsubX: ∀U : set, U ∈ Tx → U ⊆ X.
Let U be given.
Assume HU: U ∈ Tx.
We prove the intermediate claim HU_pow: U ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub U HU).
An exact proof term for the current goal is (PowerE X U HU_pow).
We prove the intermediate claim HJmeet: ∀U : set, U ∈ J → U ∩ A ≠ Empty.
Let U be given.
Assume HUJ: U ∈ J.
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ x ∈ U0) U HUJ).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ x ∈ U0) U HUJ).
An exact proof term for the current goal is (Hmeet U HUTx HxU).
We prove the intermediate claim Hg_in: ∀U : set, U ∈ J → g U ∈ U ∩ A.
Let U be given.
Assume HUJ: U ∈ J.
We prove the intermediate claim HUne: U ∩ A ≠ Empty.
An exact proof term for the current goal is (HJmeet U HUJ).
We prove the intermediate claim Hexy: ∃y : set, y ∈ U ∩ A.
An exact proof term for the current goal is (nonempty_has_element (U ∩ A) HUne).
An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ y ∈ U ∩ A) Hexy).
We prove the intermediate claim Hg_in_X: ∀U : set, U ∈ J → g U ∈ X.
Let U be given.
Assume HUJ: U ∈ J.
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ x ∈ U0) U HUJ).
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (HsubX U HUTx).
We prove the intermediate claim HgU_in_U: g U ∈ U.
An exact proof term for the current goal is (binintersectE1 U A (g U) (Hg_in U HUJ)).
An exact proof term for the current goal is (HUsub (g U) HgU_in_U).
We prove the intermediate claim Hdir: directed_set J le.
An exact proof term for the current goal is (neighborhoods_directed_by_reverse_inclusion X Tx x HTx HxX).
We prove the intermediate claim Htot: total_function_on net J X.
An exact proof term for the current goal is (total_function_on_graph J X g Hg_in_X).
We use net to witness the existential quantifier.
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
Apply andI to the current goal.
We will prove net_converges_on X Tx net J le x.
We will prove topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
Apply andI to the current goal.
We will prove topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X.
Apply and6I to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is Hdir.
An exact proof term for the current goal is Htot.
An exact proof term for the current goal is (functional_graph_graph J g).
An exact proof term for the current goal is (graph_domain_subset_graph J g).
An exact proof term for the current goal is HxX.
Let U0 be given.
Assume HU0: U0 ∈ Tx.
Assume HxU0: x ∈ U0.
We will prove ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U0.
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (SepI Tx (λU0a : set ⇒ x ∈ U0a) U0 HU0 HxU0).
Let i be given.
Assume HiJ: i ∈ J.
Assume Hlei: (U0,i) ∈ le.
We will prove apply_fun net i ∈ U0.
We prove the intermediate claim HiSub: i ⊆ U0.
An exact proof term for the current goal is (andER ((U0,i) ∈ setprod J J) (i ⊆ U0) (rev_inclusion_relE J U0 i Hlei)).
rewrite the current goal using (apply_fun_graph J g i HiJ) (from left to right).
We prove the intermediate claim Hgi_in_i: g i ∈ i.
An exact proof term for the current goal is (binintersectE1 i A (g i) (Hg_in i HiJ)).
An exact proof term for the current goal is (HiSub (g i) Hgi_in_i).
We will prove net_points_in A net J.
Let U be given.
Assume HUJ: U ∈ J.
We will prove apply_fun net U ∈ A.
rewrite the current goal using (apply_fun_graph J g U HUJ) (from left to right).
An exact proof term for the current goal is (binintersectE2 U A (g U) (Hg_in U HUJ)).
Assume Hex: ∃net J le : set, net_converges_on X Tx net J le x ∧ net_points_in A net J.
Apply Hex to the current goal.
Let net be given.
Assume Hex1: ∃J le : set, net_converges_on X Tx net J le x ∧ net_points_in A net J.
Apply Hex1 to the current goal.
Let J be given.
Assume Hex2: ∃le : set, net_converges_on X Tx net J le x ∧ net_points_in A net J.
Apply Hex2 to the current goal.
Let le be given.
Assume Hboth: net_converges_on X Tx net J le x ∧ net_points_in A net J.
Apply Hboth to the current goal.
Assume Hconv Hpts.
Apply Hconv to the current goal.
Assume Hcore Htail.
Apply Hcore to the current goal.
Assume Hcore5 HxX.
Apply Hcore5 to the current goal.
Assume Hcore4 Hdom.
Apply Hcore4 to the current goal.
Assume Hcore3 Hgraph.
Apply Hcore3 to the current goal.
Assume Hcore2 Htot.
Apply Hcore2 to the current goal.
Assume HTx0 HdirJ.
We will prove x ∈ closure_of X Tx A.
We will prove x ∈ {x0 ∈ X|∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty}.
Apply (SepI X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxX) to the current goal.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove U ∩ A ≠ Empty.
We prove the intermediate claim Hexi0: ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
An exact proof term for the current goal is (Htail U HU HxU).
Apply Hexi0 to the current goal.
Let i0 be given.
Assume Hi0pair.
Apply Hi0pair to the current goal.
Assume Hi0J Hafter.
We prove the intermediate claim Hi0refl: (i0,i0) ∈ le.
An exact proof term for the current goal is (directed_set_refl J le HdirJ i0 Hi0J).
We prove the intermediate claim HyU: apply_fun net i0 ∈ U.
An exact proof term for the current goal is (Hafter i0 Hi0J Hi0refl).
We prove the intermediate claim HyA: apply_fun net i0 ∈ A.
An exact proof term for the current goal is (Hpts i0 Hi0J).
We prove the intermediate claim HyUA: apply_fun net i0 ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A (apply_fun net i0) HyU HyA).
Assume Hempty: U ∩ A = Empty.
We prove the intermediate claim HyEmpty: apply_fun net i0 ∈ Empty.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HyUA.
An exact proof term for the current goal is (EmptyE (apply_fun net i0) HyEmpty False).
∎