Let X, Tx, F and G be given.
Assume HLF: locally_finite_family X Tx F.
Assume HGF: G ⊆ F.
We will prove locally_finite_family X Tx G.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ G ∧ ∀A : set, A ∈ G → A ∩ N ≠ Empty → A ∈ S.
Apply andI to the current goal.
An exact proof term for the current goal is (locally_finite_family_topology X Tx F HLF).
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HLFx: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (locally_finite_family_property X Tx F HLF x HxX).
Apply HLFx to the current goal.
Let N be given.
Assume HN: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.
We use N to witness the existential quantifier.
We prove the intermediate claim HNpair: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S) HN).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S) HN).
Apply andI to the current goal.
An exact proof term for the current goal is HNpair.
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HS1: finite S ∧ S ⊆ F.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ F) (∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S) HS).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ F) HS1).
We prove the intermediate claim HSsubF: S ⊆ F.
An exact proof term for the current goal is (andER (finite S) (S ⊆ F) HS1).
We prove the intermediate claim HSprop: ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ F) (∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S) HS).
Set SG to be the term {A ∈ S|A ∈ G}.
We use SG to witness the existential quantifier.
We will prove (finite SG ∧ SG ⊆ G) ∧ ∀A : set, A ∈ G → A ∩ N ≠ Empty → A ∈ SG.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HSGsub: SG ⊆ S.
An exact proof term for the current goal is (Sep_Subq S (λA : set ⇒ A ∈ G)).
An exact proof term for the current goal is (Subq_finite S HSfin SG HSGsub).
Let A be given.
Assume HA: A ∈ SG.
An exact proof term for the current goal is (SepE2 S (λA0 : set ⇒ A0 ∈ G) A HA).
Let A be given.
Assume HAG: A ∈ G.
Assume HAnN: A ∩ N ≠ Empty.
We prove the intermediate claim HAF: A ∈ F.
An exact proof term for the current goal is (HGF A HAG).
We prove the intermediate claim HAS: A ∈ S.
An exact proof term for the current goal is (HSprop A HAF HAnN).
Apply SepI to the current goal.
An exact proof term for the current goal is HAS.
An exact proof term for the current goal is HAG.
∎