Let X, Tx and x be given.
Assume Hpath: path_connected_space X Tx.
Assume HxX: x ∈ X.
We will prove path_component_of X Tx x = X.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (path_connected_space_topology X Tx Hpath).
We prove the intermediate claim Hpathprop: ∀x0 y0 : set, x0 ∈ X → y0 ∈ X → ∃p : set, path_between X x0 y0 p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
Let x0 and y0 be given.
Assume Hx0: x0 ∈ X.
Assume Hy0: y0 ∈ X.
An exact proof term for the current goal is (path_connected_space_paths X Tx x0 y0 Hpath Hx0 Hy0).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ path_component_of X Tx x.
We will prove y ∈ X.
An exact proof term for the current goal is (SepE1 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 Hy).
Let y be given.
Assume HyX: y ∈ X.
We will prove y ∈ path_component_of X Tx x.
We will prove y ∈ {y0 ∈ 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 = y0}.
Apply SepI to the current goal.
An exact proof term for the current goal is HyX.
We prove the intermediate claim Hex: ∃p : set, path_between X x y p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
An exact proof term for the current goal is (Hpathprop x y HxX HyX).
Apply Hex to the current goal.
Let p be given.
Assume Hp: path_between X x y p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
We prove the intermediate claim Hpb: path_between X x y p.
An exact proof term for the current goal is (path_witness_between X Tx x y p Hp).
We prove the intermediate claim Hcont: continuous_map unit_interval unit_interval_topology X Tx p.
An exact proof term for the current goal is (path_witness_continuous X Tx x y p Hp).
We will prove ∃q : set, function_on q unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx q ∧ apply_fun q 0 = x ∧ apply_fun q 1 = y.
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 = y.
We prove the intermediate claim HpbL: function_on p unit_interval X ∧ apply_fun p 0 = x.
An exact proof term for the current goal is (path_between_pair0 X x y p Hpb).
We prove the intermediate claim Hp1: apply_fun p 1 = y.
An exact proof term for the current goal is (path_between_at_one X x y p Hpb).
We prove the intermediate claim Hp0: apply_fun p 0 = x.
An exact proof term for the current goal is (path_between_at_zero X x y p Hpb).
We prove the intermediate claim Hfun: function_on p unit_interval X.
An exact proof term for the current goal is (path_between_function_on X x y p Hpb).
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 Hfun.
An exact proof term for the current goal is Hcont.
An exact proof term for the current goal is Hp0.
An exact proof term for the current goal is Hp1.
∎