Let X, Tx, F and x be given.
Assume HLF: locally_finite_family X Tx F.
Assume HxX: x ∈ X.
Set Fx to be the term {A ∈ F|x ∈ A}.
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 HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HNcore: 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) HNpack).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HNcore).
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) HNpack).
Apply HexS to the current goal.
Let S be given.
Assume HSpack: finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HSleft: 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) HSpack).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ F) HSleft).
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) HSpack).
We prove the intermediate claim HFxSub: Fx ⊆ S.
Let A be given.
Assume HA: A ∈ Fx.
We prove the intermediate claim HAF: A ∈ F.
An exact proof term for the current goal is (SepE1 F (λA0 : set ⇒ x ∈ A0) A HA).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (SepE2 F (λA0 : set ⇒ x ∈ A0) A HA).
We prove the intermediate claim HxAN: x ∈ A ∩ N.
An exact proof term for the current goal is (binintersectI A N x HxA HxN).
We prove the intermediate claim HAnN: A ∩ N ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (A ∩ N) x HxAN).
An exact proof term for the current goal is (HSprop A HAF HAnN).
An exact proof term for the current goal is (Subq_finite S HSfin Fx HFxSub).
∎