Let X, Tx and D be given.
Assume Hcomp: compact_space X Tx.
Assume Hclosed: ∀C : set, C ∈ D → closed_in X Tx C.
Assume Hfip: finite_intersection_property X D.
We will prove intersection_of_family X D ≠ Empty.
Assume Hempty: intersection_of_family X D = Empty.
We will prove False.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
Set Fam to be the term {X ∖ C|C ∈ D}.
We prove the intermediate claim HFamPow: Fam ⊆ 𝒫 X.
Let U be given.
Assume HU: U ∈ Fam.
Apply (ReplE D (λC0 : set ⇒ X ∖ C0) U HU) to the current goal.
Let C0 be given.
Assume H1.
Apply H1 to the current goal.
Assume HC0D: C0 ∈ D.
Assume HUeq: U = X ∖ C0.
rewrite the current goal using HUeq (from left to right).
Apply PowerI to the current goal.
An exact proof term for the current goal is (setminus_Subq X C0).
We prove the intermediate claim HFamOpen: ∀U : set, U ∈ Fam → U ∈ Tx.
Let U be given.
Assume HU: U ∈ Fam.
Apply (ReplE D (λC0 : set ⇒ X ∖ C0) U HU) to the current goal.
Let C be given.
Assume H1.
Apply H1 to the current goal.
Assume HCD: C ∈ D.
Assume HUeq: U = X ∖ C.
We prove the intermediate claim HCclosed: closed_in X Tx C.
An exact proof term for the current goal is (Hclosed C HCD).
We prove the intermediate claim HUopen: open_in X Tx (X ∖ C).
An exact proof term for the current goal is (open_of_closed_complement X Tx C HCclosed).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ C) HUopen).
We prove the intermediate claim Hcov: X ⊆ ⋃ Fam.
Let x be given.
Assume HxX: x ∈ X.
Apply (xm (x ∈ ⋃ Fam)) to the current goal.
Assume HxU: x ∈ ⋃ Fam.
An exact proof term for the current goal is HxU.
Assume HxnotU: ¬ (x ∈ ⋃ Fam).
Apply FalseE to the current goal.
We prove the intermediate claim HforallFam: ∀U : set, U ∈ Fam → ¬ (x ∈ U).
Let U be given.
Assume HUFam: U ∈ Fam.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (HxnotU (UnionI Fam x U HxU HUFam)).
We prove the intermediate claim HforallD: ∀C : set, C ∈ D → x ∈ C.
Let C be given.
Assume HCD: C ∈ D.
Apply (xm (x ∈ C)) to the current goal.
Assume HxC: x ∈ C.
An exact proof term for the current goal is HxC.
Assume HxnotC: ¬ (x ∈ C).
Apply FalseE to the current goal.
We prove the intermediate claim HxXC: x ∈ X ∖ C.
An exact proof term for the current goal is (setminusI X C x HxX HxnotC).
We prove the intermediate claim HXCUFam: X ∖ C ∈ Fam.
An exact proof term for the current goal is (ReplI D (λC0 : set ⇒ X ∖ C0) C HCD).
An exact proof term for the current goal is ((HforallFam (X ∖ C) HXCUFam) HxXC).
We prove the intermediate claim HxInt: x ∈ intersection_of_family X D.
An exact proof term for the current goal is (intersection_of_familyI X D x HxX HforallD).
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HxInt.
An exact proof term for the current goal is (EmptyE x HxEmpty False).
We prove the intermediate claim Hcover: open_cover_of X Tx Fam.
An exact proof term for the current goal is (open_cover_ofI X Tx Fam HTx HFamPow Hcov HFamOpen).
We prove the intermediate claim Hfin: has_finite_subcover X Tx Fam.
An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp Fam Hcover).
Apply Hfin to the current goal.
Let G be given.
Assume HG: G ⊆ Fam ∧ finite G ∧ X ⊆ ⋃ G.
We prove the intermediate claim HGpair: G ⊆ Fam ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ Fam ∧ finite G) (X ⊆ ⋃ G) HG).
We prove the intermediate claim HGsub: G ⊆ Fam.
An exact proof term for the current goal is (andEL (G ⊆ Fam) (finite G) HGpair).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ Fam) (finite G) HGpair).
We prove the intermediate claim HGcovers: X ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ Fam ∧ finite G) (X ⊆ ⋃ G) HG).
Set F to be the term Repl G (λU : set ⇒ X ∖ U).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (Repl_finite (λU : set ⇒ X ∖ U) G HGfin).
We prove the intermediate claim HFsubD: F ⊆ D.
Let C be given.
Assume HC: C ∈ F.
Apply (ReplE G (λU : set ⇒ X ∖ U) C HC) to the current goal.
Let U be given.
Assume HU.
Apply HU to the current goal.
Assume HUG: U ∈ G.
Assume HCeq: C = X ∖ U.
We prove the intermediate claim HUFam: U ∈ Fam.
An exact proof term for the current goal is (HGsub U HUG).
Apply (ReplE D (λC0 : set ⇒ X ∖ C0) U HUFam) to the current goal.
Let C0 be given.
Assume H1.
Apply H1 to the current goal.
Assume HC0D: C0 ∈ D.
Assume HUeq0: U = X ∖ C0.
rewrite the current goal using HCeq (from left to right).
rewrite the current goal using HUeq0 (from left to right).
We prove the intermediate claim HC0subX: C0 ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx C0 (Hclosed C0 HC0D)).
We prove the intermediate claim Hdouble: X ∖ (X ∖ C0) = C0.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X ∖ (X ∖ C0).
We will prove x ∈ C0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (X ∖ C0) x Hx).
We prove the intermediate claim HxnotXC0: x ∉ X ∖ C0.
An exact proof term for the current goal is (setminusE2 X (X ∖ C0) x Hx).
Apply (xm (x ∈ C0)) to the current goal.
Assume HxC0: x ∈ C0.
An exact proof term for the current goal is HxC0.
Assume HxnotC0: x ∉ C0.
Apply FalseE to the current goal.
We prove the intermediate claim HxXC0: x ∈ X ∖ C0.
An exact proof term for the current goal is (setminusI X C0 x HxX HxnotC0).
An exact proof term for the current goal is (HxnotXC0 HxXC0).
Let x be given.
Assume HxC0: x ∈ C0.
We will prove x ∈ X ∖ (X ∖ C0).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HC0subX x HxC0).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume HxXC0: x ∈ X ∖ C0.
We prove the intermediate claim HxnotC0: x ∉ C0.
An exact proof term for the current goal is (setminusE2 X C0 x HxXC0).
An exact proof term for the current goal is (HxnotC0 HxC0).
rewrite the current goal using Hdouble (from left to right).
An exact proof term for the current goal is HC0D.
We prove the intermediate claim HinterEmpty: intersection_of_family X F = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ intersection_of_family X F.
Apply FalseE to the current goal.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λy ⇒ ∀C0 : set, C0 ∈ F → y ∈ C0) x Hx).
We prove the intermediate claim HallF: ∀C0 : set, C0 ∈ F → x ∈ C0.
An exact proof term for the current goal is (SepE2 X (λy ⇒ ∀C0 : set, C0 ∈ F → y ∈ C0) x Hx).
We prove the intermediate claim HxnotUG: ¬ (x ∈ ⋃ G).
Assume HxUG: x ∈ ⋃ G.
Apply (UnionE_impred G x HxUG) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HUG: U ∈ G.
We prove the intermediate claim HXminusU_in_F: X ∖ U ∈ F.
An exact proof term for the current goal is (ReplI G (λU0 : set ⇒ X ∖ U0) U HUG).
We prove the intermediate claim Hx_in_XminusU: x ∈ X ∖ U.
An exact proof term for the current goal is (HallF (X ∖ U) HXminusU_in_F).
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x Hx_in_XminusU).
An exact proof term for the current goal is (HxnotU HxU).
We prove the intermediate claim HxUG: x ∈ ⋃ G.
An exact proof term for the current goal is (HGcovers x HxX).
An exact proof term for the current goal is (HxnotUG HxUG).
Let x be given.
Assume Hx: x ∈ Empty.
An exact proof term for the current goal is (EmptyE x Hx (x ∈ intersection_of_family X F)).
We prove the intermediate claim HfipCore: ∀F0 : set, finite F0 → F0 ⊆ D → intersection_of_family X F0 ≠ Empty.
An exact proof term for the current goal is (andER (D ⊆ 𝒫 X) (∀F0 : set, finite F0 → F0 ⊆ D → intersection_of_family X F0 ≠ Empty) Hfip).
We prove the intermediate claim HinterNon: intersection_of_family X F ≠ Empty.
An exact proof term for the current goal is (HfipCore F HFfin HFsubD).
An exact proof term for the current goal is (HinterNon HinterEmpty).
∎