Let X, Tx, A and B be given.
Assume HTx: topology_on X Tx.
Assume HAX: A ⊆ X.
Assume HBX: B ⊆ X.
Assume HA: connected_space A (subspace_topology X Tx A).
Assume HAB: A ⊆ B.
Assume HBcl: B ⊆ closure_of X Tx A.
We will prove connected_space B (subspace_topology X Tx B).
We will prove topology_on B (subspace_topology X Tx B) ∧ ¬ (∃U V : set, U ∈ subspace_topology X Tx B ∧ V ∈ subspace_topology X Tx B ∧ separation_of B U V).
We prove the intermediate claim HtopB: topology_on B (subspace_topology X Tx B).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx B HTx HBX).
Apply andI to the current goal.
An exact proof term for the current goal is HtopB.
We will prove ¬ (∃U V : set, U ∈ subspace_topology X Tx B ∧ V ∈ subspace_topology X Tx B ∧ separation_of B U V).
Assume HsepExists: ∃U V : set, U ∈ subspace_topology X Tx B ∧ V ∈ subspace_topology X Tx B ∧ separation_of B U V.
We will prove False.
Apply HsepExists to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ subspace_topology X Tx B ∧ V ∈ subspace_topology X Tx B ∧ separation_of B U V.
Apply HexV to the current goal.
Let V be given.
Assume HUVsep.
We prove the intermediate claim HUVopen: U ∈ subspace_topology X Tx B ∧ V ∈ subspace_topology X Tx B.
An exact proof term for the current goal is (andEL (U ∈ subspace_topology X Tx B ∧ V ∈ subspace_topology X Tx B) (separation_of B U V) HUVsep).
We prove the intermediate claim HUopen: U ∈ subspace_topology X Tx B.
An exact proof term for the current goal is (andEL (U ∈ subspace_topology X Tx B) (V ∈ subspace_topology X Tx B) HUVopen).
We prove the intermediate claim HVopen: V ∈ subspace_topology X Tx B.
An exact proof term for the current goal is (andER (U ∈ subspace_topology X Tx B) (V ∈ subspace_topology X Tx B) HUVopen).
We prove the intermediate claim Hsep: separation_of B U V.
An exact proof term for the current goal is (andER (U ∈ subspace_topology X Tx B ∧ V ∈ subspace_topology X Tx B) (separation_of B U V) HUVsep).
We prove the intermediate claim Hpart1: ((((U ∈ 𝒫 B ∧ V ∈ 𝒫 B) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 B ∧ V ∈ 𝒫 B) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = B) Hsep).
We prove the intermediate claim HAux: (((U ∈ 𝒫 B ∧ V ∈ 𝒫 B) ∧ U ∩ V = Empty) ∧ U ≠ Empty).
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 B ∧ V ∈ 𝒫 B) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim HVne: V ≠ Empty.
An exact proof term for the current goal is (andER (((U ∈ 𝒫 B ∧ V ∈ 𝒫 B) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (andER ((U ∈ 𝒫 B ∧ V ∈ 𝒫 B) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim Hpowdisj: (U ∈ 𝒫 B ∧ V ∈ 𝒫 B) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 B ∧ V ∈ 𝒫 B) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim Hpow: U ∈ 𝒫 B ∧ V ∈ 𝒫 B.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 B ∧ V ∈ 𝒫 B) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 B ∧ V ∈ 𝒫 B) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim HUpow: U ∈ 𝒫 B.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 B) (V ∈ 𝒫 B) Hpow).
We prove the intermediate claim HVpow: V ∈ 𝒫 B.
An exact proof term for the current goal is (andER (U ∈ 𝒫 B) (V ∈ 𝒫 B) Hpow).
We prove the intermediate claim HUsubB: U ⊆ B.
An exact proof term for the current goal is (PowerE B U HUpow).
We prove the intermediate claim HVsubB: V ⊆ B.
An exact proof term for the current goal is (PowerE B V HVpow).
We prove the intermediate claim HeqTopA: subspace_topology B (subspace_topology X Tx B) A = subspace_topology X Tx A.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx B A HTx HBX HAB).
We prove the intermediate claim HAconnB: connected_space A (subspace_topology B (subspace_topology X Tx B) A).
rewrite the current goal using HeqTopA (from left to right).
An exact proof term for the current goal is HA.
We prove the intermediate claim HA_side: A ⊆ U ∨ A ⊆ V.
An exact proof term for the current goal is (connected_subset_in_separation_side B (subspace_topology X Tx B) U V A HtopB HAB HAconnB HUopen HVopen Hsep).
Apply HA_side to the current goal.
Assume HAU: A ⊆ U.
We prove the intermediate claim Hexv: ∃v : set, v ∈ V.
An exact proof term for the current goal is (nonempty_has_element V HVne).
Apply Hexv to the current goal.
Let v be given.
Assume HvV: v ∈ V.
We prove the intermediate claim HvB: v ∈ B.
An exact proof term for the current goal is (HVsubB v HvV).
We prove the intermediate claim Hvcl: v ∈ closure_of X Tx A.
An exact proof term for the current goal is (HBcl v HvB).
We prove the intermediate claim HexW: ∃W ∈ Tx, V = W ∩ B.
An exact proof term for the current goal is (SepE2 (𝒫 B) (λV0 : set ⇒ ∃W ∈ Tx, V0 = W ∩ B) V HVopen).
Apply HexW to the current goal.
Let W be given.
Assume HWpair.
We prove the intermediate claim HWopen: W ∈ Tx.
An exact proof term for the current goal is (andEL (W ∈ Tx) (V = W ∩ B) HWpair).
We prove the intermediate claim HVeql: V = W ∩ B.
An exact proof term for the current goal is (andER (W ∈ Tx) (V = W ∩ B) HWpair).
We prove the intermediate claim HvWB: v ∈ W ∩ B.
rewrite the current goal using HVeql (from right to left).
An exact proof term for the current goal is HvV.
We prove the intermediate claim HvW: v ∈ W.
An exact proof term for the current goal is (binintersectE1 W B v HvWB).
We prove the intermediate claim Hclcond: ∀U0 : set, U0 ∈ Tx → v ∈ U0 → U0 ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → U0 ∩ A ≠ Empty) v Hvcl).
We prove the intermediate claim HWAnE: W ∩ A ≠ Empty.
An exact proof term for the current goal is (Hclcond W HWopen HvW).
Apply (nonempty_has_element (W ∩ A) HWAnE) to the current goal.
Let a be given.
Assume HaWA: a ∈ W ∩ A.
We prove the intermediate claim HaW: a ∈ W.
An exact proof term for the current goal is (binintersectE1 W A a HaWA).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (binintersectE2 W A a HaWA).
We prove the intermediate claim HaB: a ∈ B.
An exact proof term for the current goal is (HAB a HaA).
We prove the intermediate claim HaWB: a ∈ W ∩ B.
An exact proof term for the current goal is (binintersectI W B a HaW HaB).
We prove the intermediate claim HaV: a ∈ V.
rewrite the current goal using HVeql (from left to right).
An exact proof term for the current goal is HaWB.
We prove the intermediate claim HaU: a ∈ U.
An exact proof term for the current goal is (HAU a HaA).
We prove the intermediate claim HaUV: a ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V a HaU HaV).
We prove the intermediate claim HaE: a ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HaUV.
An exact proof term for the current goal is (EmptyE a HaE).
Assume HAV: A ⊆ V.
We prove the intermediate claim Hexu: ∃u : set, u ∈ U.
An exact proof term for the current goal is (nonempty_has_element U HUne).
Apply Hexu to the current goal.
Let u be given.
Assume HuU: u ∈ U.
We prove the intermediate claim HuB: u ∈ B.
An exact proof term for the current goal is (HUsubB u HuU).
We prove the intermediate claim Hucl: u ∈ closure_of X Tx A.
An exact proof term for the current goal is (HBcl u HuB).
We prove the intermediate claim HexW: ∃W ∈ Tx, U = W ∩ B.
An exact proof term for the current goal is (SepE2 (𝒫 B) (λU0 : set ⇒ ∃W ∈ Tx, U0 = W ∩ B) U HUopen).
Apply HexW to the current goal.
Let W be given.
Assume HWpair.
We prove the intermediate claim HWopen: W ∈ Tx.
An exact proof term for the current goal is (andEL (W ∈ Tx) (U = W ∩ B) HWpair).
We prove the intermediate claim HUeql: U = W ∩ B.
An exact proof term for the current goal is (andER (W ∈ Tx) (U = W ∩ B) HWpair).
We prove the intermediate claim HuWB: u ∈ W ∩ B.
rewrite the current goal using HUeql (from right to left).
An exact proof term for the current goal is HuU.
We prove the intermediate claim HuW: u ∈ W.
An exact proof term for the current goal is (binintersectE1 W B u HuWB).
We prove the intermediate claim Hclcond: ∀U0 : set, U0 ∈ Tx → u ∈ U0 → U0 ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → U0 ∩ A ≠ Empty) u Hucl).
We prove the intermediate claim HWAnE: W ∩ A ≠ Empty.
An exact proof term for the current goal is (Hclcond W HWopen HuW).
Apply (nonempty_has_element (W ∩ A) HWAnE) to the current goal.
Let a be given.
Assume HaWA: a ∈ W ∩ A.
We prove the intermediate claim HaW: a ∈ W.
An exact proof term for the current goal is (binintersectE1 W A a HaWA).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (binintersectE2 W A a HaWA).
We prove the intermediate claim HaB: a ∈ B.
An exact proof term for the current goal is (HAB a HaA).
We prove the intermediate claim HaWB: a ∈ W ∩ B.
An exact proof term for the current goal is (binintersectI W B a HaW HaB).
We prove the intermediate claim HaU: a ∈ U.
rewrite the current goal using HUeql (from left to right).
An exact proof term for the current goal is HaWB.
We prove the intermediate claim HaV: a ∈ V.
An exact proof term for the current goal is (HAV a HaA).
We prove the intermediate claim HaUV: a ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V a HaU HaV).
We prove the intermediate claim HaE: a ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HaUV.
An exact proof term for the current goal is (EmptyE a HaE).
∎