Let X, Tx, x and y be given.
Assume HTx: topology_on X Tx.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume HyPc: y ∈ path_component_of X Tx x.
We will prove x ∈ path_component_of X Tx y.
We will prove x ∈ {z ∈ X|∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = y ∧ apply_fun p 1 = z}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
We will prove ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = y ∧ apply_fun p 1 = x.
We prove the intermediate claim Hex: ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y0) y HyPc).
Set p0 to be the term Eps_i (λp : set ⇒ function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y).
We prove the intermediate claim Hp0prop: function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0 ∧ apply_fun p0 0 = x ∧ apply_fun p0 1 = y.
An exact proof term for the current goal is (Eps_i_ex (λp : set ⇒ function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y) Hex).
We prove the intermediate claim Hp0A: ((function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0) ∧ apply_fun p0 0 = x) ∧ apply_fun p0 1 = y.
An exact proof term for the current goal is Hp0prop.
We prove the intermediate claim Hp0B: (function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0) ∧ apply_fun p0 0 = x.
An exact proof term for the current goal is (andEL ((function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0) ∧ apply_fun p0 0 = x) (apply_fun p0 1 = y) Hp0A).
We prove the intermediate claim Hp0C: function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0.
An exact proof term for the current goal is (andEL (function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0) (apply_fun p0 0 = x) Hp0B).
We prove the intermediate claim Hp_fun: function_on p0 unit_interval X.
An exact proof term for the current goal is (andEL (function_on p0 unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx p0) Hp0C).
We prove the intermediate claim Hp_cont: continuous_map unit_interval unit_interval_topology X Tx p0.
An exact proof term for the current goal is (andER (function_on p0 unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx p0) Hp0C).
We prove the intermediate claim Hp0eq: apply_fun p0 0 = x.
An exact proof term for the current goal is (andER (function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0) (apply_fun p0 0 = x) Hp0B).
We prove the intermediate claim Hp1eq: apply_fun p0 1 = y.
An exact proof term for the current goal is (andER ((function_on p0 unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p0) ∧ apply_fun p0 0 = x) (apply_fun p0 1 = y) Hp0A).
Set q to be the term compose_fun unit_interval flip_unit_interval p0.
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 = x.
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 (function_on_compose_fun unit_interval unit_interval X flip_unit_interval p0 flip_unit_interval_function_on Hp_fun).
An exact proof term for the current goal is (composition_continuous unit_interval unit_interval_topology unit_interval unit_interval_topology X Tx flip_unit_interval p0 flip_unit_interval_continuous Hp_cont).
We prove the intermediate claim H0I: 0 ∈ unit_interval.
An exact proof term for the current goal is zero_in_unit_interval.
We prove the intermediate claim Hq0: apply_fun q 0 = apply_fun p0 (apply_fun flip_unit_interval 0).
An exact proof term for the current goal is (compose_fun_apply unit_interval flip_unit_interval p0 0 H0I).
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using flip_unit_interval_at_0 (from left to right).
rewrite the current goal using Hp1eq (from left to right).
Use reflexivity.
We prove the intermediate claim H1I: 1 ∈ unit_interval.
An exact proof term for the current goal is one_in_unit_interval.
We prove the intermediate claim Hq1: apply_fun q 1 = apply_fun p0 (apply_fun flip_unit_interval 1).
An exact proof term for the current goal is (compose_fun_apply unit_interval flip_unit_interval p0 1 H1I).
rewrite the current goal using Hq1 (from left to right).
rewrite the current goal using flip_unit_interval_at_1 (from left to right).
rewrite the current goal using Hp0eq (from left to right).
Use reflexivity.
∎