Let X, F and U be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ intersection_of_family X (F ∪ {U}).
We will prove x ∈ (intersection_of_family X F) ∩ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀T : set, T ∈ (F ∪ {U}) → x0 ∈ T) x Hx).
We prove the intermediate claim Hall: ∀T : set, T ∈ (F ∪ {U}) → x ∈ T.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀T : set, T ∈ (F ∪ {U}) → x0 ∈ T) x Hx).
We prove the intermediate claim HxInF: x ∈ intersection_of_family X F.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀T : set, T ∈ F → x0 ∈ T) x HxX (λT HT ⇒ Hall T (binunionI1 F {U} T HT))).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (Hall U (binunionI2 F {U} U (SingI U))).
An exact proof term for the current goal is (binintersectI (intersection_of_family X F) U x HxInF HxU).
Let x be given.
Assume Hx: x ∈ (intersection_of_family X F) ∩ U.
We will prove x ∈ intersection_of_family X (F ∪ {U}).
We prove the intermediate claim HxInF: x ∈ intersection_of_family X F.
An exact proof term for the current goal is (binintersectE1 (intersection_of_family X F) U x Hx).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE2 (intersection_of_family X F) U x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀T : set, T ∈ F → x0 ∈ T) x HxInF).
We prove the intermediate claim HallF: ∀T : set, T ∈ F → x ∈ T.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀T : set, T ∈ F → x0 ∈ T) x HxInF).
We prove the intermediate claim Hall: ∀T : set, T ∈ (F ∪ {U}) → x ∈ T.
Let T be given.
Assume HT.
We will prove x ∈ T.
Apply (binunionE' F {U} T (x ∈ T)) to the current goal.
Assume HTF: T ∈ F.
An exact proof term for the current goal is (HallF T HTF).
Assume HTU: T ∈ {U}.
We prove the intermediate claim HUeq: T = U.
An exact proof term for the current goal is (SingE U T HTU).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HT.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀T : set, T ∈ (F ∪ {U}) → x0 ∈ T) x HxX Hall).
∎