Let X, A, B, S, Ts, WF, C and pick be given.
Assume HTs: topology_on S Ts.
Assume HWFdef: WF = {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.
Assume HCdef: C = {pick W0|W0 ∈ WF}.
Assume Hpick: ∀W0 : set, W0 ∈ WF → pick W0 ∈ W0.
Let x be given.
Assume HxS: x ∈ S.
Let W be given.
Assume HWdef: W = component_of S Ts x.
Assume HWnotWF: ¬ (W ∈ WF).
We will prove C ∩ W = Empty.
Apply set_ext to the current goal.
Let c be given.
Assume Hc: c ∈ C ∩ W.
We will prove c ∈ Empty.
We prove the intermediate claim HcC: c ∈ C.
An exact proof term for the current goal is (binintersectE1 C W c Hc).
We prove the intermediate claim HcW: c ∈ W.
An exact proof term for the current goal is (binintersectE2 C W c Hc).
We prove the intermediate claim HcC': c ∈ {pick W0|W0 ∈ WF}.
rewrite the current goal using HCdef (from right to left).
An exact proof term for the current goal is HcC.
We prove the intermediate claim HexW0: ∃W0 ∈ WF, c = pick W0.
An exact proof term for the current goal is (ReplE WF (λW0 : set ⇒ pick W0) c HcC').
Apply HexW0 to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0WF: W0 ∈ WF.
An exact proof term for the current goal is (andEL (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim HcEq: c = pick W0.
An exact proof term for the current goal is (andER (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim HcW0: c ∈ W0.
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is (Hpick W0 HW0WF).
We prove the intermediate claim HcComp: c ∈ component_of S Ts x.
rewrite the current goal using HWdef (from right to left).
An exact proof term for the current goal is HcW.
We prove the intermediate claim HcS: c ∈ S.
An exact proof term for the current goal is (SepE1 S (λy0 : set ⇒ ∃D : set, connected_space D (subspace_topology S Ts D) ∧ x ∈ D ∧ y0 ∈ D) c HcComp).
We prove the intermediate claim HcompEqW: component_of S Ts c = component_of S Ts x.
An exact proof term for the current goal is (component_of_eq_if_in S Ts x c HTs HxS HcComp).
We prove the intermediate claim HxComp: x ∈ component_of S Ts x.
An exact proof term for the current goal is (point_in_component S Ts x HTs HxS).
We prove the intermediate claim HcompEqW': component_of S Ts x = component_of S Ts c.
rewrite the current goal using HcompEqW (from left to right).
Use reflexivity.
We prove the intermediate claim HcCompX: c ∈ component_of S Ts x.
An exact proof term for the current goal is HcComp.
We prove the intermediate claim HW0isComp: ∃y : set, y ∈ S ∧ W0 = component_of S Ts y.
An exact proof term for the current goal is (ex32_8b_WF_is_component_family X A B S Ts WF HWFdef W0 HW0WF).
Apply HW0isComp to the current goal.
Let y be given.
Assume Hpair.
We prove the intermediate claim HyS: y ∈ S.
An exact proof term for the current goal is (andEL (y ∈ S) (W0 = component_of S Ts y) Hpair).
We prove the intermediate claim HW0eqComp: W0 = component_of S Ts y.
An exact proof term for the current goal is (andER (y ∈ S) (W0 = component_of S Ts y) Hpair).
We prove the intermediate claim HcCompY: c ∈ component_of S Ts y.
rewrite the current goal using HW0eqComp (from right to left).
An exact proof term for the current goal is HcW0.
We prove the intermediate claim HcompEqW0: component_of S Ts c = component_of S Ts y.
An exact proof term for the current goal is (component_of_eq_if_in S Ts y c HTs HyS HcCompY).
We prove the intermediate claim HW0eqW: W0 = component_of S Ts x.
rewrite the current goal using HW0eqComp (from left to right).
rewrite the current goal using HcompEqW0 (from right to left).
rewrite the current goal using HcompEqW (from left to right).
Use reflexivity.
We prove the intermediate claim HWinWF: W ∈ WF.
rewrite the current goal using HWdef (from left to right).
rewrite the current goal using HW0eqW (from right to left).
An exact proof term for the current goal is HW0WF.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HWnotWF HWinWF).
An exact proof term for the current goal is (Subq_Empty (C ∩ W)).
∎