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: ∀W : set, W ∈ WF → pick W ∈ W.
Let W be given.
Assume HW: W ∈ WF.
We prove the intermediate claim HdisjWF: pairwise_disjoint WF.
An exact proof term for the current goal is (ex32_8b_WF_pairwise_disjoint X A B S Ts WF HTs HWFdef).
Apply set_ext to the current goal.
Let c be given.
Assume Hc: c ∈ C ∩ W.
We will prove c ∈ {pick W}.
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 HexW0: ∃W0 ∈ WF, c = pick W0.
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.
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 HW0: 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 HpickW0: pick W0 ∈ W0.
An exact proof term for the current goal is (Hpick W0 HW0).
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 HpickW0.
Apply (xm (W0 = W)) to the current goal.
Assume Heq: W0 = W.
rewrite the current goal using HcEq (from left to right).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI (pick W)).
Assume Hneq: W0 ≠ W.
We prove the intermediate claim Hempty: W0 ∩ W = Empty.
An exact proof term for the current goal is (HdisjWF W0 W HW0 HW Hneq).
We prove the intermediate claim HcIn: c ∈ W0 ∩ W.
An exact proof term for the current goal is (binintersectI W0 W c HcW0 HcW).
We prove the intermediate claim HcE: c ∈ Empty.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HcIn.
An exact proof term for the current goal is (EmptyE c HcE (c ∈ {pick W})).
Let c be given.
Assume Hc: c ∈ {pick W}.
We will prove c ∈ C ∩ W.
We prove the intermediate claim HcEq: c = pick W.
An exact proof term for the current goal is (SingE (pick W) c Hc).
rewrite the current goal using HcEq (from left to right).
Apply binintersectI to the current goal.
rewrite the current goal using HCdef (from left to right).
An exact proof term for the current goal is (ReplI WF (λW0 : set ⇒ pick W0) W HW).
An exact proof term for the current goal is (Hpick W HW).
∎