Let X, Tx and x be given.
Assume HTx: topology_on X Tx.
Assume HxX: x ∈ X.
We will prove x ∈ path_component_of X Tx x.
We will prove x ∈ {y ∈ X|∃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}.
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 = x ∧ apply_fun p 1 = x.
Set p to be the term const_fun unit_interval x.
We use p to witness the existential quantifier.
We will prove 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 = x.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let t be given.
Assume HtI: t ∈ unit_interval.
We will prove apply_fun p t ∈ X.
We prove the intermediate claim Hpt: apply_fun p t = x.
An exact proof term for the current goal is (const_fun_apply unit_interval x t HtI).
rewrite the current goal using Hpt (from left to right).
An exact proof term for the current goal is HxX.
We prove the intermediate claim HtopI: topology_on unit_interval unit_interval_topology.
An exact proof term for the current goal is unit_interval_topology_on.
An exact proof term for the current goal is (const_fun_continuous unit_interval unit_interval_topology X Tx x HtopI HTx HxX).
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).
An exact proof term for the current goal is (const_fun_apply unit_interval x 0 H0).
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 H1: 1 ∈ unit_interval.
An exact proof term for the current goal is (andER (0 ∈ unit_interval) (1 ∈ unit_interval) H01).
An exact proof term for the current goal is (const_fun_apply unit_interval x 1 H1).
∎