Let Fam be given.

Assume Hcover: open_cover_of X Tx Fam.

We will prove has_finite_subcover X Tx Fam.

Apply (xm (has_finite_subcover X Tx Fam)) to the current goal.

Assume Hfin: has_finite_subcover X Tx Fam.

An exact proof term for the current goal is Hfin.

Assume Hnofin: ¬ (has_finite_subcover X Tx Fam).

Apply FalseE to the current goal.

We prove the intermediate claim HXcov: X ⊆ ⋃ Fam.

An exact proof term for the current goal is (open_cover_of_covers X Tx Fam Hcover).

We prove the intermediate claim HFamOpen: ∀U : set, U ∈ Fam → U ∈ Tx.

Let U be given.

Assume HU: U ∈ Fam.

An exact proof term for the current goal is (open_cover_of_members_open X Tx Fam U Hcover HU).

Set D to be the term {X ∖ U|U ∈ Fam}.

We prove the intermediate claim HclosedD: ∀C : set, C ∈ D → closed_in X Tx C.

Let C be given.

Assume HC: C ∈ D.

Apply (ReplE Fam (λU0 : set ⇒ X ∖ U0) C HC) to the current goal.

Let U be given.

Assume H1.

Apply H1 to the current goal.

Assume HU: U ∈ Fam.

Assume HCeq: C = X ∖ U.

We prove the intermediate claim HUopen: U ∈ Tx.

An exact proof term for the current goal is (HFamOpen U HU).

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

An exact proof term for the current goal is (closed_of_open_complement X Tx U HTx HUopen).

We prove the intermediate claim HfipD: finite_intersection_property X D.

We will prove D ⊆ 𝒫 X ∧ ∀F : set, finite F → F ⊆ D → intersection_of_family X F ≠ Empty.

Apply andI to the current goal.

Let C be given.

Assume HC: C ∈ D.

Apply (ReplE Fam (λU0 : set ⇒ X ∖ U0) C HC) to the current goal.

Let U be given.

Assume H1.

Apply H1 to the current goal.

Assume HU: U ∈ Fam.

Assume HCeq: C = X ∖ U.

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

Apply PowerI to the current goal.

An exact proof term for the current goal is (setminus_Subq X U).

Let F be given.

Assume HFfin: finite F.

Assume HFsub: F ⊆ D.

Set pickU to be the term λC0 : set ⇒ Eps_i (λU0 : set ⇒ U0 ∈ Fam ∧ C0 = X ∖ U0).

Set G to be the term {pickU C0|C0 ∈ F}.

We prove the intermediate claim HGfin: finite G.

An exact proof term for the current goal is (Repl_finite pickU F HFfin).

We prove the intermediate claim HGsubFam: G ⊆ Fam.

Let U0 be given.

Assume HU0: U0 ∈ G.

Apply (ReplE F pickU U0 HU0) to the current goal.

Let C0 be given.

Assume H1.

Apply H1 to the current goal.

Assume HC0F: C0 ∈ F.

Assume HU0eq: U0 = pickU C0.

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

We prove the intermediate claim HC0D: C0 ∈ D.

An exact proof term for the current goal is (HFsub C0 HC0F).

We prove the intermediate claim HexU: ∃U1 : set, (U1 ∈ Fam ∧ C0 = X ∖ U1).

Apply (ReplE_impred Fam (λU2 : set ⇒ X ∖ U2) C0 HC0D (∃U1 : set, (U1 ∈ Fam ∧ C0 = X ∖ U1))) to the current goal.

Let U2 be given.

Assume HU2Fam: U2 ∈ Fam.

Assume HC0eq: C0 = X ∖ U2.

We use U2 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HU2Fam.

An exact proof term for the current goal is HC0eq.

We prove the intermediate claim Hpick: pickU C0 ∈ Fam ∧ C0 = X ∖ pickU C0.

An exact proof term for the current goal is (Eps_i_ex (λU1 : set ⇒ U1 ∈ Fam ∧ C0 = X ∖ U1) HexU).

An exact proof term for the current goal is (andEL (pickU C0 ∈ Fam) (C0 = X ∖ pickU C0) Hpick).

We prove the intermediate claim HnotcovG: ¬ (X ⊆ ⋃ G).

Assume HcovG: X ⊆ ⋃ G.

Apply Hnofin to the current goal.

Apply (has_finite_subcoverI X Tx Fam G) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is HGsubFam.

An exact proof term for the current goal is HGfin.

An exact proof term for the current goal is HcovG.

We prove the intermediate claim Hexx: ∃x : set, x ∈ X ∧ ¬ (x ∈ ⋃ G).

We prove the intermediate claim Hexx0: ∃x : set, ¬ (x ∈ X → x ∈ ⋃ G).

An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ X → x ∈ ⋃ G) HnotcovG).

Apply Hexx0 to the current goal.

Let x be given.

Assume Hnimp: ¬ (x ∈ X → x ∈ ⋃ G).

We use x to witness the existential quantifier.

An exact proof term for the current goal is (not_imp (x ∈ X) (x ∈ ⋃ G) Hnimp).

Apply Hexx to the current goal.

Let x be given.

Assume Hxpair: x ∈ X ∧ ¬ (x ∈ ⋃ G).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (andEL (x ∈ X) (¬ (x ∈ ⋃ G)) Hxpair).

We prove the intermediate claim HxnotUG: ¬ (x ∈ ⋃ G).

An exact proof term for the current goal is (andER (x ∈ X) (¬ (x ∈ ⋃ G)) Hxpair).

We will prove intersection_of_family X F ≠ Empty.

Apply (elem_implies_nonempty (intersection_of_family X F) x) to the current goal.

Apply (intersection_of_familyI X F x HxX) to the current goal.

Let C0 be given.

Assume HC0F: C0 ∈ F.

We prove the intermediate claim HC0D: C0 ∈ D.

An exact proof term for the current goal is (HFsub C0 HC0F).

We prove the intermediate claim HexU: ∃U0 : set, (U0 ∈ Fam ∧ C0 = X ∖ U0).

Apply (ReplE_impred Fam (λU : set ⇒ X ∖ U) C0 HC0D (∃U0 : set, (U0 ∈ Fam ∧ C0 = X ∖ U0))) to the current goal.

Let U be given.

Assume HU: U ∈ Fam.

Assume HC0eq: C0 = X ∖ U.

We use U to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HU.

An exact proof term for the current goal is HC0eq.

Set U0 to be the term pickU C0.

We prove the intermediate claim HU0prop: U0 ∈ Fam ∧ C0 = X ∖ U0.

An exact proof term for the current goal is (Eps_i_ex (λU1 : set ⇒ U1 ∈ Fam ∧ C0 = X ∖ U1) HexU).

We prove the intermediate claim HU0G: U0 ∈ G.

An exact proof term for the current goal is (ReplI F pickU C0 HC0F).

We prove the intermediate claim HxnotU0: x ∉ U0.

Assume HxU0: x ∈ U0.

An exact proof term for the current goal is (HxnotUG (UnionI G x U0 HxU0 HU0G)).

rewrite the current goal using (andER (U0 ∈ Fam) (C0 = X ∖ U0) HU0prop) (from left to right).

An exact proof term for the current goal is (setminusI X U0 x HxX HxnotU0).

We prove the intermediate claim HnonD: intersection_of_family X D ≠ Empty.

An exact proof term for the current goal is (HclosedFIP D HclosedD HfipD).

We prove the intermediate claim HinterSub: ∀x : set, x ∉ intersection_of_family X D.

Let x be given.

Assume HxD: x ∈ intersection_of_family X D.

We will prove False.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (intersection_of_familyE1 X D x HxD).

We prove the intermediate claim HallD: ∀C : set, C ∈ D → x ∈ C.

An exact proof term for the current goal is (intersection_of_familyE2 X D x HxD).

We prove the intermediate claim HxUFam: x ∈ ⋃ Fam.

An exact proof term for the current goal is (HXcov x HxX).

Apply (UnionE_impred Fam x HxUFam False) to the current goal.

Let U be given.

Assume HxU: x ∈ U.

Assume HUFam: U ∈ Fam.

We prove the intermediate claim HXminusU_in_D: X ∖ U ∈ D.

An exact proof term for the current goal is (ReplI Fam (λU0 : set ⇒ X ∖ U0) U HUFam).

We prove the intermediate claim HxXC: x ∈ X ∖ U.

An exact proof term for the current goal is (HallD (X ∖ U) HXminusU_in_D).

We prove the intermediate claim HxnotU: x ∉ U.

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

An exact proof term for the current goal is (HxnotU HxU).

We prove the intermediate claim HinterEq: intersection_of_family X D = Empty.

An exact proof term for the current goal is (Empty_eq (intersection_of_family X D) HinterSub).

An exact proof term for the current goal is (HnonD HinterEq).