Let X, Tx, Y, Ty, f and g be given.
Assume Hf: continuous_map X Tx Y Ty f.
Assume Hg: continuous_map X Tx Y Ty g.
Assume HHaus: Hausdorff_space Y Ty.
We will prove closed_in X Tx {x ∈ X|apply_fun f x = apply_fun g x}.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (topology_on Y Ty) (andEL (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) (andEL ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf))).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andEL (topology_on Y Ty) (∀y1 y2 : set, y1 ∈ Y → y2 ∈ Y → y1 ≠ y2 → ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ y1 ∈ U ∧ y2 ∈ V ∧ U ∩ V = Empty) HHaus).
Set h to be the term pair_map X f g.
We prove the intermediate claim Hhcont: continuous_map X Tx (setprod Y Y) (product_topology Y Ty Y Ty) h.
An exact proof term for the current goal is (maps_into_products_axiom X Tx Y Ty Y Ty f g Hf Hg).
Set D to be the term {(y,y)|y ∈ Y}.
We prove the intermediate claim HclosedD: closed_in (setprod Y Y) (product_topology Y Ty Y Ty) D.
An exact proof term for the current goal is (iffEL (Hausdorff_space Y Ty) (closed_in (setprod Y Y) (product_topology Y Ty Y Ty) {(y,y)|y ∈ Y}) (ex17_13_diagonal_closed_iff_Hausdorff Y Ty HTy) HHaus).
We prove the intermediate claim Hpre_closed: closed_in X Tx (preimage_of X h D).
An exact proof term for the current goal is (continuous_preserves_closed X Tx (setprod Y Y) (product_topology Y Ty Y Ty) h Hhcont D HclosedD).
We prove the intermediate claim Heq: preimage_of X h D = {x ∈ X|apply_fun f x = apply_fun g x}.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X h D.
We will prove x ∈ {x ∈ X|apply_fun f x = apply_fun g x}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun h x0 ∈ D) x Hx).
We prove the intermediate claim HhDx: apply_fun h x ∈ D.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun h x0 ∈ D) x Hx).
Apply (ReplE Y (λy : set ⇒ (y,y)) (apply_fun h x) HhDx) to the current goal.
Let y be given.
Assume HyPair.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (andEL (y ∈ Y) (apply_fun h x = (y,y)) HyPair).
We prove the intermediate claim HeqPair: apply_fun h x = (y,y).
An exact proof term for the current goal is (andER (y ∈ Y) (apply_fun h x = (y,y)) HyPair).
We prove the intermediate claim Happ: apply_fun h x = (apply_fun f x,apply_fun g x).
An exact proof term for the current goal is (pair_map_apply X Y Y f g x HxX).
We prove the intermediate claim HfgEq: (apply_fun f x,apply_fun g x) = (y,y).
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HeqPair.
We prove the intermediate claim H0: (apply_fun f x,apply_fun g x) 0 = apply_fun f x.
An exact proof term for the current goal is (tuple_2_0_eq (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim H1: (apply_fun f x,apply_fun g x) 1 = apply_fun g x.
An exact proof term for the current goal is (tuple_2_1_eq (apply_fun f x) (apply_fun g x)).
We prove the intermediate claim H0eq: (y,y) 0 = apply_fun f x.
rewrite the current goal using HfgEq (from right to left).
An exact proof term for the current goal is H0.
We prove the intermediate claim H1eq: (y,y) 1 = apply_fun g x.
rewrite the current goal using HfgEq (from right to left).
An exact proof term for the current goal is H1.
We prove the intermediate claim Hyfx: y = apply_fun f x.
rewrite the current goal using (tuple_2_0_eq y y) (from right to left).
An exact proof term for the current goal is H0eq.
We prove the intermediate claim Hygx: y = apply_fun g x.
rewrite the current goal using (tuple_2_1_eq y y) (from right to left).
An exact proof term for the current goal is H1eq.
Apply (SepI X (λx0 : set ⇒ apply_fun f x0 = apply_fun g x0) x HxX) to the current goal.
rewrite the current goal using Hyfx (from right to left).
rewrite the current goal using Hygx (from right to left).
Use reflexivity.
Let x be given.
Assume Hx: x ∈ {x ∈ X|apply_fun f x = apply_fun g x}.
We will prove x ∈ preimage_of X h D.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 = apply_fun g x0) x Hx).
We prove the intermediate claim Hfg: apply_fun f x = apply_fun g x.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 = apply_fun g x0) x Hx).
We prove the intermediate claim Hf_fun: function_on f X Y.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) (andEL ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf)).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hf_fun x HxX).
We prove the intermediate claim Happ: apply_fun h x = (apply_fun f x,apply_fun g x).
An exact proof term for the current goal is (pair_map_apply X Y Y f g x HxX).
We prove the intermediate claim Himg: apply_fun h x ∈ D.
rewrite the current goal using Happ (from left to right).
rewrite the current goal using Hfg (from right to left).
An exact proof term for the current goal is (ReplI Y (λy : set ⇒ (y,y)) (apply_fun f x) HfxY).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun h x0 ∈ D) x HxX Himg).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hpre_closed.
∎