Let x be given.

Assume Hx: x ∈ ⋃ {X ∖ u|u ∈ U}.

We will prove x ∈ X ∖ (intersection_over_family X U).

Apply (UnionE_impred {X ∖ u|u ∈ U} x Hx (x ∈ X ∖ (intersection_over_family X U))) to the current goal.

Let Y be given.

Assume HxY: x ∈ Y.

Assume HY: Y ∈ {X ∖ u|u ∈ U}.

We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ Y = X ∖ u.

An exact proof term for the current goal is (ReplE U (λu0 : set ⇒ X ∖ u0) Y HY).

Apply Hexu to the current goal.

Let u be given.

Assume Hu: u ∈ U ∧ Y = X ∖ u.

We prove the intermediate claim HuU: u ∈ U.

An exact proof term for the current goal is (andEL (u ∈ U) (Y = X ∖ u) Hu).

We prove the intermediate claim HeqY: Y = X ∖ u.

An exact proof term for the current goal is (andER (u ∈ U) (Y = X ∖ u) Hu).

We prove the intermediate claim HxXu: x ∈ X ∖ u.

rewrite the current goal using HeqY (from right to left).

An exact proof term for the current goal is HxY.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (setminusE1 X u x HxXu).

We prove the intermediate claim Hxnotu: x ∉ u.

An exact proof term for the current goal is (setminusE2 X u x HxXu).

Apply setminusI to the current goal.

An exact proof term for the current goal is HxX.

Assume HxinInt: x ∈ intersection_over_family X U.

We prove the intermediate claim Hall: ∀u0 : set, u0 ∈ U → x ∈ u0.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀u0 : set, u0 ∈ U → x0 ∈ u0) x HxinInt).

An exact proof term for the current goal is (Hxnotu (Hall u HuU)).

Let x be given.

Assume Hx: x ∈ X ∖ (intersection_over_family X U).

We will prove x ∈ ⋃ {X ∖ u|u ∈ U}.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (setminusE1 X (intersection_over_family X U) x Hx).

We prove the intermediate claim HxnotInt: x ∉ intersection_over_family X U.

An exact proof term for the current goal is (setminusE2 X (intersection_over_family X U) x Hx).

We prove the intermediate claim HnotAll: ¬ (∀u : set, u ∈ U → x ∈ u).

Assume Hall: ∀u : set, u ∈ U → x ∈ u.

Apply HxnotInt to the current goal.

We prove the intermediate claim HdefInt: intersection_over_family X U = {x0 ∈ X|∀u0 : set, u0 ∈ U → x0 ∈ u0}.

Use reflexivity.

rewrite the current goal using HdefInt (from left to right).

Apply (SepI X (λx0 : set ⇒ ∀u0 : set, u0 ∈ U → x0 ∈ u0) x HxX) to the current goal.

An exact proof term for the current goal is Hall.

We prove the intermediate claim Hexu: ∃u : set, ¬ (u ∈ U → x ∈ u).

An exact proof term for the current goal is (not_all_ex_demorgan_i (λu0 : set ⇒ u0 ∈ U → x ∈ u0) HnotAll).

Apply Hexu to the current goal.

Let u be given.

Assume Hnimp: ¬ (u ∈ U → x ∈ u).

We prove the intermediate claim Hu: u ∈ U ∧ x ∉ u.

An exact proof term for the current goal is (not_imp (u ∈ U) (x ∈ u) Hnimp).

We prove the intermediate claim HuU: u ∈ U.

An exact proof term for the current goal is (andEL (u ∈ U) (x ∉ u) Hu).

We prove the intermediate claim Hxnotu: x ∉ u.

An exact proof term for the current goal is (andER (u ∈ U) (x ∉ u) Hu).

We prove the intermediate claim HxXu: x ∈ X ∖ u.

Apply setminusI to the current goal.

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is Hxnotu.

We prove the intermediate claim Hmem: (X ∖ u) ∈ {X ∖ u0|u0 ∈ U}.

An exact proof term for the current goal is (ReplI U (λu0 : set ⇒ X ∖ u0) u HuU).

An exact proof term for the current goal is (UnionI {X ∖ u0|u0 ∈ U} x (X ∖ u) HxXu Hmem).