Let X, Tx and F be given.
Assume HTx: topology_on X Tx.
Assume HFsub: ∀C : set, C ∈ F → C ⊆ X.
Assume HF: ∀C : set, C ∈ F → connected_space C (subspace_topology X Tx C).
Assume Hcommon: ∃x : set, ∀C : set, C ∈ F → x ∈ C.
We will prove connected_space (⋃ F) (subspace_topology X Tx (⋃ F)).
We will prove topology_on (⋃ F) (subspace_topology X Tx (⋃ F)) ∧ ¬ (∃U V : set, U ∈ subspace_topology X Tx (⋃ F) ∧ V ∈ subspace_topology X Tx (⋃ F) ∧ separation_of (⋃ F) U V).
We prove the intermediate claim HFpow: F ⊆ 𝒫 X.
Let C be given.
Assume HC: C ∈ F.
We will prove C ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X C (HFsub C HC)).
We prove the intermediate claim HUnionSubX: ⋃ F ⊆ X.
An exact proof term for the current goal is (Union_Power X F HFpow).
We prove the intermediate claim HtopUnion: topology_on (⋃ F) (subspace_topology X Tx (⋃ F)).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx (⋃ F) HTx HUnionSubX).
Apply andI to the current goal.
An exact proof term for the current goal is HtopUnion.
We will prove ¬ (∃U V : set, U ∈ subspace_topology X Tx (⋃ F) ∧ V ∈ subspace_topology X Tx (⋃ F) ∧ separation_of (⋃ F) U V).
Assume HsepExists: ∃U V : set, U ∈ subspace_topology X Tx (⋃ F) ∧ V ∈ subspace_topology X Tx (⋃ F) ∧ separation_of (⋃ F) U V.
We will prove False.
Apply Hcommon to the current goal.
Let x0 be given.
Assume Hx0All: ∀C : set, C ∈ F → x0 ∈ C.
Apply HsepExists to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ subspace_topology X Tx (⋃ F) ∧ V ∈ subspace_topology X Tx (⋃ F) ∧ separation_of (⋃ F) 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 (⋃ F) ∧ V ∈ subspace_topology X Tx (⋃ F).
An exact proof term for the current goal is (andEL (U ∈ subspace_topology X Tx (⋃ F) ∧ V ∈ subspace_topology X Tx (⋃ F)) (separation_of (⋃ F) U V) HUVsep).
We prove the intermediate claim HUopen: U ∈ subspace_topology X Tx (⋃ F).
An exact proof term for the current goal is (andEL (U ∈ subspace_topology X Tx (⋃ F)) (V ∈ subspace_topology X Tx (⋃ F)) HUVopen).
We prove the intermediate claim HVopen: V ∈ subspace_topology X Tx (⋃ F).
An exact proof term for the current goal is (andER (U ∈ subspace_topology X Tx (⋃ F)) (V ∈ subspace_topology X Tx (⋃ F)) HUVopen).
We prove the intermediate claim Hsep: separation_of (⋃ F) U V.
An exact proof term for the current goal is (andER (U ∈ subspace_topology X Tx (⋃ F) ∧ V ∈ subspace_topology X Tx (⋃ F)) (separation_of (⋃ F) U V) HUVsep).
We prove the intermediate claim Hpart1: ((((U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = ⋃ F) Hsep).
We prove the intermediate claim Hunion: U ∪ V = ⋃ F.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = ⋃ F) Hsep).
We prove the intermediate claim HAux: (((U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ U ∩ V = Empty) ∧ U ≠ Empty).
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ 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 ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim Hpowdisj: (U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (andER ((U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim Hpow: U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F).
An exact proof term for the current goal is (andEL (U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 (⋃ F) ∧ V ∈ 𝒫 (⋃ F)) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim HUpow: U ∈ 𝒫 (⋃ F).
An exact proof term for the current goal is (andEL (U ∈ 𝒫 (⋃ F)) (V ∈ 𝒫 (⋃ F)) Hpow).
We prove the intermediate claim HVpow: V ∈ 𝒫 (⋃ F).
An exact proof term for the current goal is (andER (U ∈ 𝒫 (⋃ F)) (V ∈ 𝒫 (⋃ F)) Hpow).
We prove the intermediate claim HUsub: U ⊆ ⋃ F.
An exact proof term for the current goal is (PowerE (⋃ F) U HUpow).
We prove the intermediate claim HVsub: V ⊆ ⋃ F.
An exact proof term for the current goal is (PowerE (⋃ F) V HVpow).
We prove the intermediate claim Hexv0: ∃v0 : set, v0 ∈ V.
An exact proof term for the current goal is (nonempty_has_element V HVne).
Apply Hexv0 to the current goal.
Let v0 be given.
Assume Hv0V: v0 ∈ V.
We prove the intermediate claim Hv0Union: v0 ∈ ⋃ F.
An exact proof term for the current goal is (HVsub v0 Hv0V).
Apply (UnionE_impred F v0 Hv0Union) to the current goal.
Let C0 be given.
Assume Hv0C0: v0 ∈ C0.
Assume HC0F: C0 ∈ F.
We prove the intermediate claim Hx0C0: x0 ∈ C0.
An exact proof term for the current goal is (Hx0All C0 HC0F).
We prove the intermediate claim Hx0Union: x0 ∈ ⋃ F.
An exact proof term for the current goal is (UnionI F x0 C0 Hx0C0 HC0F).
We prove the intermediate claim Hx0UV: x0 ∈ U ∪ V.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is Hx0Union.
Apply (binunionE U V x0 Hx0UV) to the current goal.
Assume Hx0U: x0 ∈ U.
We prove the intermediate claim HUnionSubU: ⋃ F ⊆ U.
Let y be given.
Assume HyUnion: y ∈ ⋃ F.
We will prove y ∈ U.
Apply (UnionE_impred F y HyUnion (y ∈ U)) to the current goal.
Let C be given.
Assume HyC: y ∈ C.
Assume HC: C ∈ F.
We prove the intermediate claim HCsubUnion: C ⊆ ⋃ F.
Let z be given.
Assume Hz: z ∈ C.
An exact proof term for the current goal is (UnionI F z C Hz HC).
We prove the intermediate claim HeqTop: subspace_topology (⋃ F) (subspace_topology X Tx (⋃ F)) C = subspace_topology X Tx C.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx (⋃ F) C HTx HUnionSubX HCsubUnion).
We prove the intermediate claim HCconn: connected_space C (subspace_topology (⋃ F) (subspace_topology X Tx (⋃ F)) C).
rewrite the current goal using HeqTop (from left to right).
An exact proof term for the current goal is (HF C HC).
We prove the intermediate claim HCside: C ⊆ U ∨ C ⊆ V.
An exact proof term for the current goal is (connected_subset_in_separation_side (⋃ F) (subspace_topology X Tx (⋃ F)) U V C HtopUnion HCsubUnion HCconn HUopen HVopen Hsep).
Apply HCside to the current goal.
Assume HCsubU: C ⊆ U.
An exact proof term for the current goal is (HCsubU y HyC).
Assume HCsubV: C ⊆ V.
We prove the intermediate claim Hx0C: x0 ∈ C.
An exact proof term for the current goal is (Hx0All C HC).
We prove the intermediate claim Hx0V: x0 ∈ V.
An exact proof term for the current goal is (HCsubV x0 Hx0C).
We prove the intermediate claim Hx0UV2: x0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x0 Hx0U Hx0V).
We prove the intermediate claim Hx0E: x0 ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is Hx0UV2.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x0 Hx0E).
We prove the intermediate claim HVsubU: V ⊆ U.
Let y be given.
Assume HyV: y ∈ V.
An exact proof term for the current goal is (HUnionSubU y (HVsub y HyV)).
We prove the intermediate claim HVsubEmpty: V ⊆ Empty.
Let y be given.
Assume HyV: y ∈ V.
We will prove y ∈ Empty.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (HVsubU y HyV).
We prove the intermediate claim HyUV: y ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V y HyU HyV).
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HyUV.
We prove the intermediate claim HVEmpty: V = Empty.
An exact proof term for the current goal is (Empty_Subq_eq V HVsubEmpty).
An exact proof term for the current goal is (HVne HVEmpty).
Assume Hx0V: x0 ∈ V.
We prove the intermediate claim HUnionSubV: ⋃ F ⊆ V.
Let y be given.
Assume HyUnion: y ∈ ⋃ F.
We will prove y ∈ V.
Apply (UnionE_impred F y HyUnion (y ∈ V)) to the current goal.
Let C be given.
Assume HyC: y ∈ C.
Assume HC: C ∈ F.
We prove the intermediate claim HCsubUnion: C ⊆ ⋃ F.
Let z be given.
Assume Hz: z ∈ C.
An exact proof term for the current goal is (UnionI F z C Hz HC).
We prove the intermediate claim HeqTop: subspace_topology (⋃ F) (subspace_topology X Tx (⋃ F)) C = subspace_topology X Tx C.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx (⋃ F) C HTx HUnionSubX HCsubUnion).
We prove the intermediate claim HCconn: connected_space C (subspace_topology (⋃ F) (subspace_topology X Tx (⋃ F)) C).
rewrite the current goal using HeqTop (from left to right).
An exact proof term for the current goal is (HF C HC).
We prove the intermediate claim HCside: C ⊆ U ∨ C ⊆ V.
An exact proof term for the current goal is (connected_subset_in_separation_side (⋃ F) (subspace_topology X Tx (⋃ F)) U V C HtopUnion HCsubUnion HCconn HUopen HVopen Hsep).
Apply HCside to the current goal.
Assume HCsubU: C ⊆ U.
We prove the intermediate claim Hx0C: x0 ∈ C.
An exact proof term for the current goal is (Hx0All C HC).
We prove the intermediate claim Hx0U: x0 ∈ U.
An exact proof term for the current goal is (HCsubU x0 Hx0C).
We prove the intermediate claim Hx0UV2: x0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x0 Hx0U Hx0V).
We prove the intermediate claim Hx0E: x0 ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is Hx0UV2.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x0 Hx0E).
Assume HCsubV: C ⊆ V.
An exact proof term for the current goal is (HCsubV y HyC).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is HUne.
We prove the intermediate claim HUsubV: U ⊆ V.
Let y be given.
Assume HyU: y ∈ U.
An exact proof term for the current goal is (HUnionSubV y (HUsub y HyU)).
We prove the intermediate claim HUsubEmpty: U ⊆ Empty.
Let y be given.
Assume HyU: y ∈ U.
We will prove y ∈ Empty.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (HUsubV y HyU).
We prove the intermediate claim HyUV: y ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V y HyU HyV).
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HyUV.
We prove the intermediate claim HUEmpty: U = Empty.
An exact proof term for the current goal is (Empty_Subq_eq U HUsubEmpty).
An exact proof term for the current goal is (HUne HUEmpty).
∎