Assume Hcont: continuous_map X Tx Y Ty f.

We will prove ∀net J le x : set, net_converges_on X Tx net J le x → net_converges_on Y Ty (compose_fun J net f) J le (apply_fun f x).

Let net, J, le and x be given.

Assume Hnetconv: net_converges_on X Tx net J le x.

We prove the intermediate claim HfXY: 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 Hpre: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.

An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hcont).

Apply Hnetconv 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 net_converges_on Y Ty (compose_fun J net f) J le (apply_fun f x).

We will prove topology_on Y Ty ∧ directed_set J le ∧ total_function_on (compose_fun J net f) J Y ∧ functional_graph (compose_fun J net f) ∧ graph_domain_subset (compose_fun J net f) J ∧ (apply_fun f x) ∈ Y ∧ ∀V : set, V ∈ Ty → apply_fun f x ∈ V → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun (compose_fun J net f) i ∈ V.

Apply andI to the current goal.

Apply and6I to the current goal.

An exact proof term for the current goal is HTy.

An exact proof term for the current goal is HdirJ.

We prove the intermediate claim Hnetfun: function_on net J X.

An exact proof term for the current goal is (total_function_on_function_on net J X Htot).

An exact proof term for the current goal is (total_function_on_compose_fun J X Y net f Hnetfun HfXY).

An exact proof term for the current goal is (functional_graph_compose_fun J net f).

An exact proof term for the current goal is (graph_domain_subset_compose_fun J net f).

An exact proof term for the current goal is (HfXY x HxX).

Let V be given.

Assume HV: V ∈ Ty.

Assume HfxV: apply_fun f x ∈ V.

Set W to be the term preimage_of X f V.

We prove the intermediate claim HWTx: W ∈ Tx.

An exact proof term for the current goal is (Hpre V HV).

We prove the intermediate claim HxW: x ∈ W.

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

We prove the intermediate claim Hexi0: ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ W.

An exact proof term for the current goal is (Htail W HWTx HxW).

Apply Hexi0 to the current goal.

Let i0 be given.

Assume Hi0pair.

Apply Hi0pair to the current goal.

Assume Hi0J Hafter.

We use i0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hi0J.

Let i be given.

Assume HiJ: i ∈ J.

Assume Hi0i: (i0,i) ∈ le.

We will prove apply_fun (compose_fun J net f) i ∈ V.

We prove the intermediate claim HnetiW: apply_fun net i ∈ W.

An exact proof term for the current goal is (Hafter i HiJ Hi0i).

We prove the intermediate claim HnetiV: apply_fun f (apply_fun net i) ∈ V.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) (apply_fun net i) HnetiW).

We prove the intermediate claim Happ: apply_fun (compose_fun J net f) i = apply_fun f (apply_fun net i).

An exact proof term for the current goal is (compose_fun_apply J net f i HiJ).

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

An exact proof term for the current goal is HnetiV.

Assume Hnets: ∀net J le x : set, net_converges_on X Tx net J le x → net_converges_on Y Ty (compose_fun J net f) J le (apply_fun f x).

We will prove continuous_map X Tx Y Ty f.

We will prove topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y ∧ ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is HTy.

We will prove function_on f X Y.

Let x be given.

Assume HxX: x ∈ X.

Set J0 to be the term {x}.

Set le0 to be the term setprod J0 J0.

Set net0 to be the term graph J0 (λ_ : set ⇒ x).

We prove the intermediate claim Hdir0: directed_set J0 le0.

We will prove directed_set J0 le0.

We will prove (J0 ≠ Empty ∧ partial_order_on J0 le0) ∧ ∀a b : set, a ∈ J0 → b ∈ J0 → ∃c : set, c ∈ J0 ∧ (a,c) ∈ le0 ∧ (b,c) ∈ le0.

Apply andI to the current goal.

An exact proof term for the current goal is (elem_implies_nonempty J0 x (SingI x)).

We will prove partial_order_on J0 le0.

We will prove ((relation_on le0 J0 ∧ (∀a : set, a ∈ J0 → (a,a) ∈ le0)) ∧ (∀a b : set, a ∈ J0 → b ∈ J0 → (a,b) ∈ le0 → (b,a) ∈ le0 → a = b)) ∧ (∀a b c : set, a ∈ J0 → b ∈ J0 → c ∈ J0 → (a,b) ∈ le0 → (b,c) ∈ le0 → (a,c) ∈ le0).

Apply andI to the current goal.

We will prove relation_on le0 J0.

Let a and b be given.

Assume Hab: (a,b) ∈ le0.

We will prove a ∈ J0 ∧ b ∈ J0.

We prove the intermediate claim Ha0: (a,b) 0 ∈ J0.

An exact proof term for the current goal is (ap0_Sigma J0 (λ_ : set ⇒ J0) (a,b) Hab).

We prove the intermediate claim Hb1: (a,b) 1 ∈ J0.

An exact proof term for the current goal is (ap1_Sigma J0 (λ_ : set ⇒ J0) (a,b) Hab).

Apply andI to the current goal.

rewrite the current goal using (tuple_2_0_eq a b) (from right to left).

An exact proof term for the current goal is Ha0.

rewrite the current goal using (tuple_2_1_eq a b) (from right to left).

An exact proof term for the current goal is Hb1.

Let a be given.

Assume HaJ: a ∈ J0.

We prove the intermediate claim HaEq: a = x.

An exact proof term for the current goal is (SingE x a HaJ).

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J0 J0 x x (SingI x) (SingI x)).

Let a and b be given.

Assume HaJ: a ∈ J0.

Assume HbJ: b ∈ J0.

Assume Hab: (a,b) ∈ le0.

Assume Hba: (b,a) ∈ le0.

We will prove a = b.

rewrite the current goal using (SingE x a HaJ) (from left to right).

rewrite the current goal using (SingE x b HbJ) (from left to right).

Use reflexivity.

Let a, b and c be given.

Assume HaJ: a ∈ J0.

Assume HbJ: b ∈ J0.

Assume HcJ: c ∈ J0.

Assume Hab: (a,b) ∈ le0.

Assume Hbc: (b,c) ∈ le0.

We will prove (a,c) ∈ le0.

We prove the intermediate claim HaEq: a = x.

An exact proof term for the current goal is (SingE x a HaJ).

We prove the intermediate claim HcEq: c = x.

An exact proof term for the current goal is (SingE x c HcJ).

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

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J0 J0 x x (SingI x) (SingI x)).

Let a and b be given.

Assume HaJ: a ∈ J0.

Assume HbJ: b ∈ J0.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (SingI x).

We prove the intermediate claim HaEq: a = x.

An exact proof term for the current goal is (SingE x a HaJ).

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J0 J0 x x (SingI x) (SingI x)).

We prove the intermediate claim HbEq: b = x.

An exact proof term for the current goal is (SingE x b HbJ).

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J0 J0 x x (SingI x) (SingI x)).

We prove the intermediate claim Hnet0conv: net_converges_on X Tx net0 J0 le0 x.

We will prove net_converges_on X Tx net0 J0 le0 x.

We will prove topology_on X Tx ∧ directed_set J0 le0 ∧ total_function_on net0 J0 X ∧ functional_graph net0 ∧ graph_domain_subset net0 J0 ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J0 ∧ ∀i : set, i ∈ J0 → (i0,i) ∈ le0 → apply_fun net0 i ∈ U.

Apply andI to the current goal.

We will prove topology_on X Tx ∧ directed_set J0 le0 ∧ total_function_on net0 J0 X ∧ functional_graph net0 ∧ graph_domain_subset net0 J0 ∧ 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 Hdir0.

We prove the intermediate claim Hgconst: ∀j : set, j ∈ J0 → (λ_ : set ⇒ x) j ∈ X.

Let j be given.

Assume Hj: j ∈ J0.

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is (total_function_on_graph J0 X (λ_ : set ⇒ x) Hgconst).

An exact proof term for the current goal is (functional_graph_graph J0 (λ_ : set ⇒ x)).

An exact proof term for the current goal is (graph_domain_subset_graph J0 (λ_ : set ⇒ x)).

An exact proof term for the current goal is HxX.

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (SingI x).

Let i be given.

Assume Hi: i ∈ J0.

Assume Hle: (x,i) ∈ le0.

rewrite the current goal using (apply_fun_graph J0 (λ_ : set ⇒ x) i Hi) (from left to right).

An exact proof term for the current goal is HxU.

We prove the intermediate claim Himg0: net_converges_on Y Ty (compose_fun J0 net0 f) J0 le0 (apply_fun f x).

An exact proof term for the current goal is (Hnets net0 J0 le0 x Hnet0conv).

Apply Himg0 to the current goal.

Assume Hcore0 Htail0.

Apply Hcore0 to the current goal.

Assume Hcore05 HfxY.

An exact proof term for the current goal is HfxY.

Let V be given.

Assume HV: V ∈ Ty.

Set W to be the term preimage_of X f V.

We will prove W ∈ Tx.

Set Fam to be the term {U ∈ Tx|U ⊆ W}.

We prove the intermediate claim HFamPow: Fam ∈ 𝒫 Tx.

Apply PowerI to the current goal.

Let U be given.

Assume HU: U ∈ Fam.

An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ U0 ⊆ W) U HU).

We prove the intermediate claim Hnbhd: ∀x0 : set, x0 ∈ W → ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ W.

Let x0 be given.

Assume Hx0W: x0 ∈ W.

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (SepE1 X (λz : set ⇒ apply_fun f z ∈ V) x0 Hx0W).

We prove the intermediate claim Hfx0V: apply_fun f x0 ∈ V.

An exact proof term for the current goal is (SepE2 X (λz : set ⇒ apply_fun f z ∈ V) x0 Hx0W).

We prove the intermediate claim Hnotcl: x0 ∉ closure_of X Tx (X ∖ W).

Apply (xm (x0 ∈ closure_of X Tx (X ∖ W))) to the current goal.

Assume Hcl: x0 ∈ closure_of X Tx (X ∖ W).

We prove the intermediate claim Hexnet: ∃net J le : set, net_converges_on X Tx net J le x0 ∧ net_points_in (X ∖ W) net J.

An exact proof term for the current goal is (iffEL (x0 ∈ closure_of X Tx (X ∖ W)) (∃net J le : set, net_converges_on X Tx net J le x0 ∧ net_points_in (X ∖ W) net J) (closure_via_nets X Tx (X ∖ W) x0 HTx) Hcl).

Apply Hexnet to the current goal.

Let net be given.

Assume Hex1: ∃J le : set, net_converges_on X Tx net J le x0 ∧ net_points_in (X ∖ W) net J.

Apply Hex1 to the current goal.

Let J be given.

Assume Hex2: ∃le : set, net_converges_on X Tx net J le x0 ∧ net_points_in (X ∖ W) net J.

Apply Hex2 to the current goal.

Let le be given.

Assume Hboth: net_converges_on X Tx net J le x0 ∧ net_points_in (X ∖ W) net J.

Apply Hboth to the current goal.

Assume Hconv Hpts.

We prove the intermediate claim Himg: net_converges_on Y Ty (compose_fun J net f) J le (apply_fun f x0).

An exact proof term for the current goal is (Hnets net J le x0 Hconv).

Apply Himg to the current goal.

Assume Hcore Htail.

Apply Hcore to the current goal.

Assume Hcore5 Hfx0Y.

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 HTy0 Hdir.

We prove the intermediate claim Hexi0: ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun (compose_fun J net f) i ∈ V.

An exact proof term for the current goal is (Htail V HV Hfx0V).

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 Hleft: J ≠ Empty ∧ partial_order_on J le.

An exact proof term for the current goal is (andEL (J ≠ Empty ∧ partial_order_on J le) (∀a b : set, a ∈ J → b ∈ J → ∃c : set, c ∈ J ∧ (a,c) ∈ le ∧ (b,c) ∈ le) Hdir).

We prove the intermediate claim Hpo: partial_order_on J le.

An exact proof term for the current goal is (andER (J ≠ Empty) (partial_order_on J le) Hleft).

We prove the intermediate claim Hrefl: ∀a : set, a ∈ J → (a,a) ∈ le.

An exact proof term for the current goal is (partial_order_on_refl J le Hpo).

We prove the intermediate claim Hrefl0: (i0,i0) ∈ le.

An exact proof term for the current goal is (Hrefl i0 Hi0J).

We prove the intermediate claim HnotV: apply_fun (compose_fun J net f) i0 ∉ V.

We prove the intermediate claim Hneti0: apply_fun net i0 ∈ X ∖ W.

An exact proof term for the current goal is (Hpts i0 Hi0J).

We prove the intermediate claim Hi0X: apply_fun net i0 ∈ X.

An exact proof term for the current goal is (setminusE1 X W (apply_fun net i0) Hneti0).

We prove the intermediate claim Hi0notW: apply_fun net i0 ∉ W.

An exact proof term for the current goal is (setminusE2 X W (apply_fun net i0) Hneti0).

Assume Hbad: apply_fun (compose_fun J net f) i0 ∈ V.

We prove the intermediate claim Happ: apply_fun (compose_fun J net f) i0 = apply_fun f (apply_fun net i0).

An exact proof term for the current goal is (compose_fun_apply J net f i0 Hi0J).

We prove the intermediate claim Hfi0V: apply_fun f (apply_fun net i0) ∈ V.

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

An exact proof term for the current goal is Hbad.

We prove the intermediate claim Hi0W: apply_fun net i0 ∈ W.

An exact proof term for the current goal is (SepI X (λz : set ⇒ apply_fun f z ∈ V) (apply_fun net i0) Hi0X Hfi0V).

An exact proof term for the current goal is (Hi0notW Hi0W False).

We prove the intermediate claim Hv: apply_fun (compose_fun J net f) i0 ∈ V.

An exact proof term for the current goal is (Hafter i0 Hi0J Hrefl0).

Assume Hcl2: x0 ∈ closure_of X Tx (X ∖ W).

An exact proof term for the current goal is (HnotV Hv).

Assume Hncl: x0 ∉ closure_of X Tx (X ∖ W).

An exact proof term for the current goal is Hncl.

Apply (xm (∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ W)) to the current goal.

Assume Hex.

An exact proof term for the current goal is Hex.

Assume Hno.

Apply FalseE to the current goal.

We prove the intermediate claim Hx0cl: x0 ∈ closure_of X Tx (X ∖ W).

We will prove x0 ∈ {z ∈ X|∀U : set, U ∈ Tx → z ∈ U → U ∩ (X ∖ W) ≠ Empty}.

Apply (SepI X (λz : set ⇒ ∀U : set, U ∈ Tx → z ∈ U → U ∩ (X ∖ W) ≠ Empty) x0 Hx0X) to the current goal.

Let U be given.

Assume HU: U ∈ Tx.

Assume Hx0U: x0 ∈ U.

We will prove U ∩ (X ∖ W) ≠ Empty.

Assume Hemp: U ∩ (X ∖ W) = Empty.

We prove the intermediate claim HUsW: U ⊆ W.

Let y be given.

Assume HyU: y ∈ U.

We will prove y ∈ W.

Apply (xm (y ∈ W)) to the current goal.

Assume HyW: y ∈ W.

An exact proof term for the current goal is HyW.

Assume HyNW: y ∉ W.

We prove the intermediate claim HyX: y ∈ X.

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (PowerE X U ((topology_sub_Power X Tx HTx) U HU)).

An exact proof term for the current goal is (HUsubX y HyU).

We prove the intermediate claim HyInComp: y ∈ X ∖ W.

An exact proof term for the current goal is (setminusI X W y HyX HyNW).

We prove the intermediate claim HyInInt: y ∈ U ∩ (X ∖ W).

An exact proof term for the current goal is (binintersectI U (X ∖ W) y HyU HyInComp).

We prove the intermediate claim HyEmpty: y ∈ Empty.

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

An exact proof term for the current goal is HyInInt.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE y HyEmpty).

Apply Hno to the current goal.

We use U to witness the existential quantifier.

We will prove (U ∈ Tx ∧ x0 ∈ U) ∧ U ⊆ W.

Apply andI to the current goal.

An exact proof term for the current goal is HU.

An exact proof term for the current goal is Hx0U.

An exact proof term for the current goal is HUsW.

An exact proof term for the current goal is (Hnotcl Hx0cl).

We prove the intermediate claim HUnionEq: ⋃ Fam = W.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ ⋃ Fam.

Apply (UnionE_impred Fam y Hy (y ∈ W)) to the current goal.

Let U be given.

Assume HyU: y ∈ U.

Assume HUFam: U ∈ Fam.

We prove the intermediate claim HUsub: U ⊆ W.

An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ U0 ⊆ W) U HUFam).

An exact proof term for the current goal is (HUsub y HyU).

Let y be given.

Assume HyW: y ∈ W.

We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ y ∈ U ∧ U ⊆ W.

An exact proof term for the current goal is (Hnbhd y HyW).

Apply HexU to the current goal.

Let U be given.

Assume HUpack: U ∈ Tx ∧ y ∈ U ∧ U ⊆ W.

We prove the intermediate claim Hleft: U ∈ Tx ∧ y ∈ U.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ y ∈ U) (U ⊆ W) HUpack).

We prove the intermediate claim HU: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (y ∈ U) Hleft).

We prove the intermediate claim HyU: y ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx) (y ∈ U) Hleft).

We prove the intermediate claim HUsW: U ⊆ W.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ y ∈ U) (U ⊆ W) HUpack).

We prove the intermediate claim HUFam: U ∈ Fam.

An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ U0 ⊆ W) U HU HUsW).

An exact proof term for the current goal is (UnionI Fam y U HyU HUFam).

We prove the intermediate claim HUnionOpen: ⋃ Fam ∈ Tx.

An exact proof term for the current goal is (topology_union_axiom X Tx HTx Fam HFamPow).

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

An exact proof term for the current goal is HUnionOpen.