Let X, Tx, V, y and z be given.
Assume HTx: topology_on X Tx.
Assume HVsubX: V ⊆ X.
Assume HpathV: path_connected_space V (subspace_topology X Tx V).
Assume HyV: y ∈ V.
Assume HzV: z ∈ V.
We will prove z ∈ path_component_of X Tx y.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HVsubX y HyV).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HVsubX z HzV).
We prove the intermediate claim HtopV: topology_on V (subspace_topology X Tx V).
An exact proof term for the current goal is (path_connected_space_topology V (subspace_topology X Tx V) HpathV).
We prove the intermediate claim Hpaths: ∀x0 y0 : set, x0 ∈ V → y0 ∈ V → ∃p : set, path_between V x0 y0 p ∧ continuous_map unit_interval unit_interval_topology V (subspace_topology X Tx V) p.
Let x0 and y0 be given.
Assume Hx0: x0 ∈ V.
Assume Hy0: y0 ∈ V.
An exact proof term for the current goal is (path_connected_space_paths V (subspace_topology X Tx V) x0 y0 HpathV Hx0 Hy0).
We prove the intermediate claim Hex: ∃p : set, path_between V y z p ∧ continuous_map unit_interval unit_interval_topology V (subspace_topology X Tx V) p.
An exact proof term for the current goal is (Hpaths y z HyV HzV).
Apply Hex to the current goal.
Let p be given.
Assume Hp: path_between V y z p ∧ continuous_map unit_interval unit_interval_topology V (subspace_topology X Tx V) p.
We prove the intermediate claim Hpb: path_between V y z p.
An exact proof term for the current goal is (path_witness_between V (subspace_topology X Tx V) y z p Hp).
We prove the intermediate claim HpcontV: continuous_map unit_interval unit_interval_topology V (subspace_topology X Tx V) p.
An exact proof term for the current goal is (path_witness_continuous V (subspace_topology X Tx V) y z p Hp).
We prove the intermediate claim HpbL: function_on p unit_interval V ∧ apply_fun p 0 = y.
An exact proof term for the current goal is (path_between_pair0 V y z p Hpb).
We prove the intermediate claim Hp1: apply_fun p 1 = z.
An exact proof term for the current goal is (path_between_at_one V y z p Hpb).
We prove the intermediate claim Hp0: apply_fun p 0 = y.
An exact proof term for the current goal is (path_between_at_zero V y z p Hpb).
We prove the intermediate claim HpfunV: function_on p unit_interval V.
An exact proof term for the current goal is (path_between_function_on V y z p Hpb).
Set j to be the term {(y0,y0)|y0 ∈ V}.
We prove the intermediate claim Hjdef: j = {(y0,y0)|y0 ∈ V}.
Use reflexivity.
We prove the intermediate claim Hjfun: function_on j V X.
Let v be given.
Assume HvV: v ∈ V.
We will prove apply_fun j v ∈ X.
We prove the intermediate claim Hjv: apply_fun j v = v.
rewrite the current goal using Hjdef (from left to right).
An exact proof term for the current goal is (identity_function_apply V v HvV).
rewrite the current goal using Hjv (from left to right).
An exact proof term for the current goal is (HVsubX v HvV).
Set q to be the term compose_fun unit_interval p j.
We prove the intermediate claim Hqfun: function_on q unit_interval X.
An exact proof term for the current goal is (function_on_compose_fun unit_interval V X p j HpfunV Hjfun).
We prove the intermediate claim HcontJ: continuous_map V (subspace_topology X Tx V) X Tx j.
We will prove topology_on V (subspace_topology X Tx V) ∧ topology_on X Tx ∧ function_on j V X ∧ ∀U : set, U ∈ Tx → preimage_of V j U ∈ subspace_topology X Tx V.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HtopV.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is Hjfun.
Let U be given.
Assume HU: U ∈ Tx.
We will prove preimage_of V j U ∈ subspace_topology X Tx V.
We prove the intermediate claim Heq: preimage_of V j U = U ∩ V.
Apply set_ext to the current goal.
Let v be given.
Assume Hv: v ∈ preimage_of V j U.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (SepE1 V (λv0 : set ⇒ apply_fun j v0 ∈ U) v Hv).
We prove the intermediate claim HjinU: apply_fun j v ∈ U.
An exact proof term for the current goal is (SepE2 V (λv0 : set ⇒ apply_fun j v0 ∈ U) v Hv).
We prove the intermediate claim Hjv0: apply_fun {(y0,y0)|y0 ∈ V} v = v.
An exact proof term for the current goal is (identity_function_apply V v HvV).
We prove the intermediate claim HjinU0: apply_fun {(y0,y0)|y0 ∈ V} v ∈ U.
rewrite the current goal using Hjdef (from right to left).
An exact proof term for the current goal is HjinU.
We prove the intermediate claim HvU: v ∈ U.
rewrite the current goal using Hjv0 (from right to left).
An exact proof term for the current goal is HjinU0.
An exact proof term for the current goal is (binintersectI U V v HvU HvV).
Let v be given.
Assume Hv: v ∈ U ∩ V.
Apply (binintersectE U V v Hv) to the current goal.
Assume HvU: v ∈ U.
Assume HvV: v ∈ V.
We will prove v ∈ preimage_of V j U.
We will prove v ∈ {v0 ∈ V|apply_fun j v0 ∈ U}.
Apply SepI to the current goal.
An exact proof term for the current goal is HvV.
We prove the intermediate claim Hjv0: apply_fun {(y0,y0)|y0 ∈ V} v = v.
An exact proof term for the current goal is (identity_function_apply V v HvV).
We will prove apply_fun j v ∈ U.
rewrite the current goal using Hjdef (from left to right).
We prove the intermediate claim HvU0: apply_fun {(y0,y0)|y0 ∈ V} v ∈ U.
rewrite the current goal using Hjv0 (from left to right).
An exact proof term for the current goal is HvU.
An exact proof term for the current goal is HvU0.
rewrite the current goal using Heq (from left to right).
We will prove U ∩ V ∈ subspace_topology X Tx V.
We will prove U ∩ V ∈ {W ∈ 𝒫 V|∃V0 ∈ Tx, W = V0 ∩ V}.
Apply SepI to the current goal.
Apply PowerI to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 U V).
We will prove ∃V0 ∈ Tx, U ∩ V = V0 ∩ V.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
Use reflexivity.
We prove the intermediate claim Hqcont: continuous_map unit_interval unit_interval_topology X Tx q.
An exact proof term for the current goal is (composition_continuous unit_interval unit_interval_topology V (subspace_topology X Tx V) X Tx p j HpcontV HcontJ).
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 H0I: 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 H1I: 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 Hq0: apply_fun q 0 = y.
We prove the intermediate claim Hq0def: apply_fun q 0 = apply_fun j (apply_fun p 0).
An exact proof term for the current goal is (compose_fun_apply unit_interval p j 0 H0I).
rewrite the current goal using Hq0def (from left to right).
rewrite the current goal using Hp0 (from left to right).
We prove the intermediate claim Hjy: apply_fun j y = y.
rewrite the current goal using Hjdef (from left to right).
An exact proof term for the current goal is (identity_function_apply V y HyV).
rewrite the current goal using Hjy (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: apply_fun q 1 = z.
We prove the intermediate claim Hq1def: apply_fun q 1 = apply_fun j (apply_fun p 1).
An exact proof term for the current goal is (compose_fun_apply unit_interval p j 1 H1I).
rewrite the current goal using Hq1def (from left to right).
rewrite the current goal using Hp1 (from left to right).
We prove the intermediate claim Hjz: apply_fun j z = z.
rewrite the current goal using Hjdef (from left to right).
An exact proof term for the current goal is (identity_function_apply V z HzV).
rewrite the current goal using Hjz (from left to right).
Use reflexivity.
We will prove z ∈ {y0 ∈ X|∃q0 : set, function_on q0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q0 ∧ apply_fun q0 0 = y ∧ apply_fun q0 1 = y0}.
Apply SepI to the current goal.
An exact proof term for the current goal is HzX.
We will prove ∃q0 : set, function_on q0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q0 ∧ apply_fun q0 0 = y ∧ apply_fun q0 1 = z.
We use q to witness the existential quantifier.
We will prove function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q ∧ apply_fun q 0 = y ∧ apply_fun q 1 = z.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hqfun.
An exact proof term for the current goal is Hqcont.
An exact proof term for the current goal is Hq0.
An exact proof term for the current goal is Hq1.
∎