Let X and Fam be given.
Assume Hsub: ∀A : set, A ∈ Fam → A ⊆ X.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ intersection_over_family X {X ∖ A|A ∈ Fam}.
We will prove x ∈ X ∖ ⋃ Fam.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ {X ∖ A|A ∈ Fam} → x0 ∈ U0) x Hx).
We prove the intermediate claim Hall: ∀U0 : set, U0 ∈ {X ∖ A|A ∈ Fam} → x ∈ U0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ {X ∖ A|A ∈ Fam} → x0 ∈ U0) x Hx).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume HxUnion: x ∈ ⋃ Fam.
Apply (UnionE_impred Fam x HxUnion (False)) to the current goal.
Let A be given.
Assume HxA: x ∈ A.
Assume HA: A ∈ Fam.
We prove the intermediate claim HXminusA: (X ∖ A) ∈ {X ∖ A0|A0 ∈ Fam}.
An exact proof term for the current goal is (ReplI Fam (λA0 : set ⇒ X ∖ A0) A HA).
We prove the intermediate claim HxXminusA: x ∈ X ∖ A.
An exact proof term for the current goal is (Hall (X ∖ A) HXminusA).
An exact proof term for the current goal is (setminusE2 X A x HxXminusA HxA).
Let x be given.
Assume Hx: x ∈ X ∖ ⋃ Fam.
We will prove x ∈ intersection_over_family X {X ∖ A|A ∈ Fam}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (⋃ Fam) x Hx).
We prove the intermediate claim HdefInt: intersection_over_family X {X ∖ A|A ∈ Fam} = {x0 ∈ X|∀U0 : set, U0 ∈ {X ∖ A|A ∈ Fam} → x0 ∈ U0}.
Use reflexivity.
rewrite the current goal using HdefInt (from left to right).
Apply (SepI X (λx0 : set ⇒ ∀U0 : set, U0 ∈ {X ∖ A|A ∈ Fam} → x0 ∈ U0) x HxX) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ {X ∖ A|A ∈ Fam}.
We will prove x ∈ U0.
We prove the intermediate claim HexA: ∃A : set, A ∈ Fam ∧ U0 = X ∖ A.
An exact proof term for the current goal is (ReplE Fam (λA0 : set ⇒ X ∖ A0) U0 HU0).
Apply HexA to the current goal.
Let A be given.
Assume HA: A ∈ Fam ∧ U0 = X ∖ A.
We prove the intermediate claim HAin: A ∈ Fam.
An exact proof term for the current goal is (andEL (A ∈ Fam) (U0 = X ∖ A) HA).
We prove the intermediate claim HU0eq: U0 = X ∖ A.
An exact proof term for the current goal is (andER (A ∈ Fam) (U0 = X ∖ A) HA).
rewrite the current goal using HU0eq (from left to right).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume HxA: x ∈ A.
Apply (setminusE2 X (⋃ Fam) x Hx) to the current goal.
An exact proof term for the current goal is (UnionI Fam x A HxA HAin).
∎