Let X, S, U and x be given.
Assume HS: subbasis_on X S.
Assume HU: U ∈ generated_topology_from_subbasis X S.
Assume HxU: x ∈ U.
We will prove ∃F : set, F ∈ finite_subcollections S ∧ x ∈ intersection_of_family X F ∧ intersection_of_family X F ⊆ U.
We prove the intermediate claim Hexb: ∃b : set, b ∈ basis_of_subbasis X S ∧ x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (generated_topology_from_subbasis_local_basis X S U x HU HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbtrip.
We prove the intermediate claim Hb12: b ∈ basis_of_subbasis X S ∧ x ∈ b.
An exact proof term for the current goal is (andEL (b ∈ basis_of_subbasis X S ∧ x ∈ b) (b ⊆ U) Hbtrip).
We prove the intermediate claim HbB: b ∈ basis_of_subbasis X S.
An exact proof term for the current goal is (andEL (b ∈ basis_of_subbasis X S) (x ∈ b) Hb12).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andER (b ∈ basis_of_subbasis X S) (x ∈ b) Hb12).
We prove the intermediate claim HbSubU: b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ basis_of_subbasis X S ∧ x ∈ b) (b ⊆ U) Hbtrip).
We prove the intermediate claim HexF: ∃F : set, F ∈ finite_subcollections S ∧ b = intersection_of_family X F ∧ b ≠ Empty.
An exact proof term for the current goal is (basis_of_subbasisE X S b HbB).
Apply HexF to the current goal.
Let F be given.
Assume HFpack.
We use F to witness the existential quantifier.
We prove the intermediate claim HF12: F ∈ finite_subcollections S ∧ b = intersection_of_family X F.
An exact proof term for the current goal is (andEL (F ∈ finite_subcollections S ∧ b = intersection_of_family X F) (b ≠ Empty) HFpack).
We prove the intermediate claim HbNe: b ≠ Empty.
An exact proof term for the current goal is (andER (F ∈ finite_subcollections S ∧ b = intersection_of_family X F) (b ≠ Empty) HFpack).
We prove the intermediate claim HFfin: F ∈ finite_subcollections S.
An exact proof term for the current goal is (andEL (F ∈ finite_subcollections S) (b = intersection_of_family X F) HF12).
We prove the intermediate claim HbEq: b = intersection_of_family X F.
An exact proof term for the current goal is (andER (F ∈ finite_subcollections S) (b = intersection_of_family X F) HF12).
We prove the intermediate claim HxInt: x ∈ intersection_of_family X F.
rewrite the current goal using HbEq (from right to left) at position 1.
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HintSubU: intersection_of_family X F ⊆ U.
Let y be given.
Assume Hy: y ∈ intersection_of_family X F.
We will prove y ∈ U.
We prove the intermediate claim Hyb: y ∈ b.
rewrite the current goal using HbEq (from left to right) at position 1.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is (HbSubU y Hyb).
We prove the intermediate claim Hleft: F ∈ finite_subcollections S ∧ x ∈ intersection_of_family X F.
An exact proof term for the current goal is (andI (F ∈ finite_subcollections S) (x ∈ intersection_of_family X F) HFfin HxInt).
An exact proof term for the current goal is (andI (F ∈ finite_subcollections S ∧ x ∈ intersection_of_family X F) (intersection_of_family X F ⊆ U) Hleft HintSubU).
∎