Let X, T and F be given.
Assume HTtop: topology_on X T.
Assume HFpow: F ∈ 𝒫 T.
Assume HFin: finite F.
We will prove intersection_of_family X F ∈ T.
We prove the intermediate claim HpEmpty: Empty ∈ 𝒫 T → intersection_of_family X Empty ∈ T.
Assume HpowEmpty.
rewrite the current goal using (intersection_of_family_empty_eq X) (from left to right).
An exact proof term for the current goal is (topology_has_X X T HTtop).
We prove the intermediate claim HpStep: ∀F0 y : set, finite F0 → y ∉ F0 → (F0 ∈ 𝒫 T → intersection_of_family X F0 ∈ T) → ((F0 ∪ {y}) ∈ 𝒫 T → intersection_of_family X (F0 ∪ {y}) ∈ T).
Let F0 and y be given.
Assume HFin0 HyNotin IH.
Assume HpowUnion: (F0 ∪ {y}) ∈ 𝒫 T.
We prove the intermediate claim HsubUnion: F0 ∪ {y} ⊆ T.
An exact proof term for the current goal is (PowerE T (F0 ∪ {y}) HpowUnion).
We prove the intermediate claim HsubF0: F0 ⊆ T.
Let U be given.
Assume HU: U ∈ F0.
An exact proof term for the current goal is (HsubUnion U (binunionI1 F0 {y} U HU)).
We prove the intermediate claim HF0pow: F0 ∈ 𝒫 T.
An exact proof term for the current goal is (PowerI T F0 HsubF0).
We prove the intermediate claim HinterF0: intersection_of_family X F0 ∈ T.
An exact proof term for the current goal is (IH HF0pow).
We prove the intermediate claim HyT: y ∈ T.
An exact proof term for the current goal is (HsubUnion y (binunionI2 F0 {y} y (SingI y))).
rewrite the current goal using (intersection_of_family_adjoin X F0 y) (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X T (intersection_of_family X F0) y HTtop HinterF0 HyT).
We prove the intermediate claim Hall: ∀F0 : set, finite F0 → (F0 ∈ 𝒫 T → intersection_of_family X F0 ∈ T).
An exact proof term for the current goal is (finite_ind (λF0 : set ⇒ F0 ∈ 𝒫 T → intersection_of_family X F0 ∈ T) HpEmpty HpStep).
We prove the intermediate claim Hspec: F ∈ 𝒫 T → intersection_of_family X F ∈ T.
An exact proof term for the current goal is (Hall F HFin).
An exact proof term for the current goal is (Hspec HFpow).
∎