Let X and Tx be given.
Assume Hpath: path_connected_space X Tx.
We will prove connected_space X Tx.
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 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 X Tx ∧ ¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We will prove ¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V).
Assume HsepX: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V.
Apply HsepX to the current goal.
Let U be given.
Assume HsepX_V: ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V.
Apply HsepX_V to the current goal.
Let V be given.
Assume HUV.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (V ∈ Tx) (andEL (U ∈ Tx ∧ V ∈ Tx) (separation_of X U V) HUV)).
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (andER (U ∈ Tx) (V ∈ Tx) (andEL (U ∈ Tx ∧ V ∈ Tx) (separation_of X U V) HUV)).
We prove the intermediate claim HsepXUV: separation_of X U V.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx) (separation_of X U V) HUV).
We prove the intermediate claim Helems: (∃x : set, x ∈ U) ∧ (∃y : set, y ∈ V).
An exact proof term for the current goal is (separation_has_elements X U V HsepXUV).
We prove the intermediate claim HexU: ∃x : set, x ∈ U.
An exact proof term for the current goal is (andEL (∃x : set, x ∈ U) (∃y : set, y ∈ V) Helems).
We prove the intermediate claim HexV: ∃y : set, y ∈ V.
An exact proof term for the current goal is (andER (∃x : set, x ∈ U) (∃y : set, y ∈ V) Helems).
Apply HexU to the current goal.
Let x be given.
Assume Hx: x ∈ U.
Apply HexV to the current goal.
Let y be given.
Assume Hy: y ∈ V.
We prove the intermediate claim Hsubsets: U ⊆ X ∧ V ⊆ X.
An exact proof term for the current goal is (separation_subsets X U V HsepXUV).
We prove the intermediate claim HU_sub: U ⊆ X.
An exact proof term for the current goal is (andEL (U ⊆ X) (V ⊆ X) Hsubsets).
We prove the intermediate claim HV_sub: V ⊆ X.
An exact proof term for the current goal is (andER (U ⊆ X) (V ⊆ X) Hsubsets).
We prove the intermediate claim HxinX: x ∈ X.
An exact proof term for the current goal is (subset_elem U X x HU_sub Hx).
We prove the intermediate claim HyinX: y ∈ X.
An exact proof term for the current goal is (subset_elem V X y HV_sub Hy).
We prove the intermediate claim Hpathxy: ∃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 (Hpath_prop x y HxinX HyinX).
Apply Hpathxy to the current goal.
Let p be given.
Assume Hp_and_cont.
We prove the intermediate claim Hp: path_between X x y p.
An exact proof term for the current goal is (path_witness_between X Tx x y p Hp_and_cont).
We prove the intermediate claim Hpcont: 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_and_cont).
We prove the intermediate claim Hpfunc: function_on p unit_interval X.
An exact proof term for the current goal is (path_between_function_on X x y p Hp).
We prove the intermediate claim Hp0eq: apply_fun p 0 = x.
An exact proof term for the current goal is (path_between_at_zero X x y p Hp).
We prove the intermediate claim Hp1eq: apply_fun p 1 = y.
An exact proof term for the current goal is (path_between_at_one X x y p Hp).
We prove the intermediate claim Hsep_left: ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = X) HsepXUV).
We prove the intermediate claim Hsep_mid: ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty.
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hsep_left).
We prove the intermediate claim Hsep_pow_disj: (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) Hsep_mid).
We prove the intermediate claim HdisjUV: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) (U ∩ V = Empty) Hsep_pow_disj).
We prove the intermediate claim HunionUV: U ∪ V = X.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = X) HsepXUV).
Set preU to be the term preimage_of unit_interval p U.
Set preV to be the term preimage_of unit_interval p V.
We prove the intermediate claim Hsep_UV: separation_of unit_interval preU preV.
We will prove preU ∈ 𝒫 unit_interval ∧ preV ∈ 𝒫 unit_interval ∧ preU ∩ preV = Empty ∧ preU ≠ Empty ∧ preV ≠ Empty ∧ preU ∪ preV = unit_interval.
Apply andI to the current goal.
We will prove ((((preU ∈ 𝒫 unit_interval ∧ preV ∈ 𝒫 unit_interval) ∧ preU ∩ preV = Empty) ∧ preU ≠ Empty) ∧ preV ≠ Empty).
Apply andI to the current goal.
We will prove (((preU ∈ 𝒫 unit_interval ∧ preV ∈ 𝒫 unit_interval) ∧ preU ∩ preV = Empty) ∧ preU ≠ Empty).
Apply andI to the current goal.
We will prove ((preU ∈ 𝒫 unit_interval ∧ preV ∈ 𝒫 unit_interval) ∧ preU ∩ preV = Empty).
Apply andI to the current goal.
We will prove preU ∈ 𝒫 unit_interval ∧ preV ∈ 𝒫 unit_interval.
Apply andI to the current goal.
We will prove preU ∈ 𝒫 unit_interval.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ preU.
An exact proof term for the current goal is (SepE1 unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ U) t Ht).
We will prove preV ∈ 𝒫 unit_interval.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ preV.
An exact proof term for the current goal is (SepE1 unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ V) t Ht).
We will prove preU ∩ preV = Empty.
Apply Empty_eq to the current goal.
Let t be given.
Assume Ht: t ∈ preU ∩ preV.
Apply (binintersectE preU preV t Ht) to the current goal.
Assume HtU: t ∈ preU.
Assume HtV: t ∈ preV.
We prove the intermediate claim HpU: apply_fun p t ∈ U.
An exact proof term for the current goal is (SepE2 unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ U) t HtU).
We prove the intermediate claim HpV: apply_fun p t ∈ V.
An exact proof term for the current goal is (SepE2 unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ V) t HtV).
We prove the intermediate claim HpUV: apply_fun p t ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V (apply_fun p t) HpU HpV).
We prove the intermediate claim Hfalse: apply_fun p t ∈ Empty.
rewrite the current goal using HdisjUV (from right to left).
An exact proof term for the current goal is HpUV.
An exact proof term for the current goal is (EmptyE (apply_fun p t) Hfalse).
Assume Heq: preU = Empty.
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 HxU: apply_fun p 0 ∈ U.
rewrite the current goal using Hp0eq (from left to right).
An exact proof term for the current goal is Hx.
We prove the intermediate claim H0pre: 0 ∈ preU.
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ U) 0 H0I HxU).
We prove the intermediate claim Hsub: preU ⊆ Empty.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Subq_ref Empty).
We prove the intermediate claim H0Empty: 0 ∈ Empty.
An exact proof term for the current goal is (Hsub 0 H0pre).
An exact proof term for the current goal is (EmptyE 0 H0Empty).
Assume Heq: preV = Empty.
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 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 HyV: apply_fun p 1 ∈ V.
rewrite the current goal using Hp1eq (from left to right).
An exact proof term for the current goal is Hy.
We prove the intermediate claim H1pre: 1 ∈ preV.
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ V) 1 H1I HyV).
We prove the intermediate claim Hsub: preV ⊆ Empty.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Subq_ref Empty).
We prove the intermediate claim H1Empty: 1 ∈ Empty.
An exact proof term for the current goal is (Hsub 1 H1pre).
An exact proof term for the current goal is (EmptyE 1 H1Empty).
We will prove preU ∪ preV = unit_interval.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preU ∪ preV.
We will prove t ∈ unit_interval.
Apply (binunionE preU preV t Ht) to the current goal.
Assume HtU: t ∈ preU.
An exact proof term for the current goal is (SepE1 unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ U) t HtU).
Assume HtV: t ∈ preV.
An exact proof term for the current goal is (SepE1 unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ V) t HtV).
Let t be given.
Assume HtI: t ∈ unit_interval.
We will prove t ∈ preU ∪ preV.
We prove the intermediate claim HptX: apply_fun p t ∈ X.
An exact proof term for the current goal is (Hpfunc t HtI).
We prove the intermediate claim HptUV: apply_fun p t ∈ U ∪ V.
rewrite the current goal using HunionUV (from left to right).
An exact proof term for the current goal is HptX.
Apply (binunionE U V (apply_fun p t) HptUV) to the current goal.
Assume HptU: apply_fun p t ∈ U.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ U) t HtI HptU).
Assume HptV: apply_fun p t ∈ V.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ apply_fun p t0 ∈ V) t HtI HptV).
We prove the intermediate claim HpreimgU: preU ∈ unit_interval_topology.
An exact proof term for the current goal is (andER (topology_on unit_interval unit_interval_topology ∧ topology_on X Tx ∧ function_on p unit_interval X) (∀V0 : set, V0 ∈ Tx → preimage_of unit_interval p V0 ∈ unit_interval_topology) Hpcont U HU).
We prove the intermediate claim HpreimgV: preV ∈ unit_interval_topology.
An exact proof term for the current goal is (andER (topology_on unit_interval unit_interval_topology ∧ topology_on X Tx ∧ function_on p unit_interval X) (∀V0 : set, V0 ∈ Tx → preimage_of unit_interval p V0 ∈ unit_interval_topology) Hpcont V HV).
We prove the intermediate claim Hsep_exists: ∃U0 V0 : set, U0 ∈ unit_interval_topology ∧ V0 ∈ unit_interval_topology ∧ separation_of unit_interval U0 V0.
We use preU to witness the existential quantifier.
We use preV to witness the existential quantifier.
We will prove preU ∈ unit_interval_topology ∧ preV ∈ unit_interval_topology ∧ separation_of unit_interval preU preV.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HpreimgU.
An exact proof term for the current goal is HpreimgV.
An exact proof term for the current goal is Hsep_UV.
We prove the intermediate claim Hunit_nosep: ¬ (∃U0 V0 : set, U0 ∈ unit_interval_topology ∧ V0 ∈ unit_interval_topology ∧ separation_of unit_interval U0 V0).
An exact proof term for the current goal is (andER (topology_on unit_interval unit_interval_topology) (¬ (∃U0 V0 : set, U0 ∈ unit_interval_topology ∧ V0 ∈ unit_interval_topology ∧ separation_of unit_interval U0 V0)) unit_interval_connected).
Apply Hunit_nosep to the current goal.
An exact proof term for the current goal is Hsep_exists.
∎