Let X, Tx, x and y be given.
Assume Hcr: completely_regular_space X Tx.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume Hxy: x ≠ y.
We will prove ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ apply_fun f y = 1.
We prove the intermediate claim Hrest: one_point_sets_closed X Tx ∧ ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1.
An exact proof term for the current goal is (andER (topology_on X Tx) (one_point_sets_closed X Tx ∧ ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1) Hcr).
We prove the intermediate claim HT1: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1) Hrest).
We prove the intermediate claim HyCl: closed_in X Tx {y}.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) HT1 y HyX).
We prove the intermediate claim Hxnoty: x ∉ {y}.
Assume Hxy0: x ∈ {y}.
We prove the intermediate claim Heq: x = y.
An exact proof term for the current goal is (SingE y x Hxy0).
An exact proof term for the current goal is (Hxy Heq).
We prove the intermediate claim Hsep: ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1) Hrest).
Apply (Hsep x HxX {y} HyCl Hxnoty) to the current goal.
Let f be given.
Assume Hfpack: continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀z : set, z ∈ {y} → apply_fun f z = 1.
We use f to witness the existential quantifier.
We prove the intermediate claim Hcont: continuous_map X Tx R R_standard_topology f.
We prove the intermediate claim Hpair: continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0) (∀z : set, z ∈ {y} → apply_fun f z = 1) Hfpack).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f) (apply_fun f x = 0) Hpair).
We prove the intermediate claim Hfx0: apply_fun f x = 0.
We prove the intermediate claim Hpair: continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0) (∀z : set, z ∈ {y} → apply_fun f z = 1) Hfpack).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f) (apply_fun f x = 0) Hpair).
We prove the intermediate claim Hfy1: apply_fun f y = 1.
We prove the intermediate claim Hfor: ∀z : set, z ∈ {y} → apply_fun f z = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0) (∀z : set, z ∈ {y} → apply_fun f z = 1) Hfpack).
An exact proof term for the current goal is (Hfor y (SingI y)).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hcont.
An exact proof term for the current goal is Hfx0.
An exact proof term for the current goal is Hfy1.
∎