Let X, Tx, Y, Ty and f be given.
Assume Hpath: path_connected_space X Tx.
Assume Hf: continuous_map X Tx Y Ty f.
Assume Hsurj: ∀y : set, y ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y.
We will prove path_connected_space Y Ty.
We prove the intermediate claim Hf_left: (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y.
An exact proof term for the current goal is (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 (andER (topology_on X Tx) (topology_on Y Ty) (andEL (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Hf_left)).
We prove the intermediate claim Hpath_prop: ∀x y : set, x ∈ X → y ∈ X → ∃p : set, path_between X x y p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
Let x and y be given.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
An exact proof term for the current goal is (path_connected_space_paths X Tx x y Hpath Hx Hy).
We will prove topology_on Y Ty ∧ ∀y1 y2 : set, y1 ∈ Y → y2 ∈ Y → ∃p : set, path_between Y y1 y2 p ∧ continuous_map unit_interval unit_interval_topology Y Ty p.
Apply andI to the current goal.
An exact proof term for the current goal is HTy.
Let y1 and y2 be given.
Assume Hy1: y1 ∈ Y.
Assume Hy2: y2 ∈ Y.
We will prove ∃p : set, path_between Y y1 y2 p ∧ continuous_map unit_interval unit_interval_topology Y Ty p.
Apply (Hsurj y1 Hy1) to the current goal.
Let x1 be given.
Assume Hx1pair: x1 ∈ X ∧ apply_fun f x1 = y1.
Apply (Hsurj y2 Hy2) to the current goal.
Let x2 be given.
Assume Hx2pair: x2 ∈ X ∧ apply_fun f x2 = y2.
We prove the intermediate claim Hx1X: x1 ∈ X.
An exact proof term for the current goal is (andEL (x1 ∈ X) (apply_fun f x1 = y1) Hx1pair).
We prove the intermediate claim Hfx1: apply_fun f x1 = y1.
An exact proof term for the current goal is (andER (x1 ∈ X) (apply_fun f x1 = y1) Hx1pair).
We prove the intermediate claim Hx2X: x2 ∈ X.
An exact proof term for the current goal is (andEL (x2 ∈ X) (apply_fun f x2 = y2) Hx2pair).
We prove the intermediate claim Hfx2: apply_fun f x2 = y2.
An exact proof term for the current goal is (andER (x2 ∈ X) (apply_fun f x2 = y2) Hx2pair).
Apply (Hpath_prop x1 x2 Hx1X Hx2X) to the current goal.
Let p be given.
Assume Hp_pair: path_between X x1 x2 p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
We prove the intermediate claim Hp_between: path_between X x1 x2 p.
An exact proof term for the current goal is (path_witness_between X Tx x1 x2 p Hp_pair).
We prove the intermediate claim Hp_cont: continuous_map unit_interval unit_interval_topology X Tx p.
An exact proof term for the current goal is (path_witness_continuous X Tx x1 x2 p Hp_pair).
Set q to be the term compose_fun unit_interval p f.
We prove the intermediate claim Hq_cont: continuous_map unit_interval unit_interval_topology Y Ty q.
An exact proof term for the current goal is (composition_continuous unit_interval unit_interval_topology X Tx Y Ty p f Hp_cont Hf).
We prove the intermediate claim Hq_left: (topology_on unit_interval unit_interval_topology ∧ topology_on Y Ty) ∧ function_on q unit_interval Y.
An exact proof term for the current goal is (andEL ((topology_on unit_interval unit_interval_topology ∧ topology_on Y Ty) ∧ function_on q unit_interval Y) (∀V : set, V ∈ Ty → preimage_of unit_interval q V ∈ unit_interval_topology) Hq_cont).
We prove the intermediate claim Hq_fun: function_on q unit_interval Y.
An exact proof term for the current goal is (andER (topology_on unit_interval unit_interval_topology ∧ topology_on Y Ty) (function_on q unit_interval Y) Hq_left).
We prove the intermediate claim H01: 0 ∈ unit_interval ∧ 1 ∈ unit_interval.
An exact proof term for the current goal is zero_one_in_unit_interval.
We prove the intermediate claim H0: 0 ∈ unit_interval.
An exact proof term for the current goal is (andEL (0 ∈ unit_interval) (1 ∈ unit_interval) H01).
We prove the intermediate claim H1: 1 ∈ unit_interval.
An exact proof term for the current goal is (andER (0 ∈ unit_interval) (1 ∈ unit_interval) H01).
We prove the intermediate claim Hp_left: function_on p unit_interval X ∧ apply_fun p 0 = x1.
An exact proof term for the current goal is (path_between_pair0 X x1 x2 p Hp_between).
We prove the intermediate claim Hp0: apply_fun p 0 = x1.
An exact proof term for the current goal is (path_between_at_zero X x1 x2 p Hp_between).
We prove the intermediate claim Hp1: apply_fun p 1 = x2.
An exact proof term for the current goal is (path_between_at_one X x1 x2 p Hp_between).
We prove the intermediate claim Hq0: apply_fun q 0 = y1.
We prove the intermediate claim Hq0a: apply_fun q 0 = apply_fun f (apply_fun p 0).
An exact proof term for the current goal is (compose_fun_apply unit_interval p f 0 H0).
rewrite the current goal using Hq0a (from left to right).
rewrite the current goal using Hp0 (from left to right).
rewrite the current goal using Hfx1 (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: apply_fun q 1 = y2.
We prove the intermediate claim Hq1a: apply_fun q 1 = apply_fun f (apply_fun p 1).
An exact proof term for the current goal is (compose_fun_apply unit_interval p f 1 H1).
rewrite the current goal using Hq1a (from left to right).
rewrite the current goal using Hp1 (from left to right).
rewrite the current goal using Hfx2 (from left to right).
Use reflexivity.
We use q to witness the existential quantifier.
We will prove path_between Y y1 y2 q ∧ continuous_map unit_interval unit_interval_topology Y Ty q.
Apply andI to the current goal.
We will prove function_on q unit_interval Y ∧ apply_fun q 0 = y1 ∧ apply_fun q 1 = y2.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hq_fun.
An exact proof term for the current goal is Hq0.
An exact proof term for the current goal is Hq1.
An exact proof term for the current goal is Hq_cont.
∎