Let X, A, B, S, Ts and WF be given.
Assume HTs: topology_on S Ts.
Assume HWFdef: WF = {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.
We prove the intermediate claim Hpart: covers S {component_of S Ts x|x ∈ S} ∧ pairwise_disjoint {component_of S Ts x|x ∈ S}.
An exact proof term for the current goal is (components_partition_space S Ts HTs).
We prove the intermediate claim HdisjComp: pairwise_disjoint {component_of S Ts x|x ∈ S}.
An exact proof term for the current goal is (andER (covers S {component_of S Ts x|x ∈ S}) (pairwise_disjoint {component_of S Ts x|x ∈ S}) Hpart).
We will prove pairwise_disjoint WF.
Let U and V be given.
Assume HU: U ∈ WF.
Assume HV: V ∈ WF.
Assume Hneq: U ≠ V.
We will prove U ∩ V = Empty.
We prove the intermediate claim HexU: ∃x : set, x ∈ S ∧ U = component_of S Ts x.
An exact proof term for the current goal is (ex32_8b_WF_is_component_family X A B S Ts WF HWFdef U HU).
We prove the intermediate claim HexV: ∃y : set, y ∈ S ∧ V = 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 V HV).
Apply HexU to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (U = component_of S Ts x) Hxpair).
We prove the intermediate claim HUeq: U = component_of S Ts x.
An exact proof term for the current goal is (andER (x ∈ S) (U = component_of S Ts x) Hxpair).
Apply HexV to the current goal.
Let y be given.
Assume Hypair.
We prove the intermediate claim HyS: y ∈ S.
An exact proof term for the current goal is (andEL (y ∈ S) (V = component_of S Ts y) Hypair).
We prove the intermediate claim HVeql: V = component_of S Ts y.
An exact proof term for the current goal is (andER (y ∈ S) (V = component_of S Ts y) Hypair).
We prove the intermediate claim HUinFam: U ∈ {component_of S Ts x0|x0 ∈ S}.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (ReplI S (λx0 : set ⇒ component_of S Ts x0) x HxS).
We prove the intermediate claim HVinFam: V ∈ {component_of S Ts x0|x0 ∈ S}.
rewrite the current goal using HVeql (from left to right).
An exact proof term for the current goal is (ReplI S (λx0 : set ⇒ component_of S Ts x0) y HyS).
An exact proof term for the current goal is (HdisjComp U V HUinFam HVinFam Hneq).
∎