Let X, Tx and A be given.
Assume Hreg: regular_space X Tx.
Assume HAcov: open_cover X Tx A.
Assume Hcond2: Michael_cond41_3_2 X Tx.
We will prove ∃D : set, closed_cover X Tx D ∧ locally_finite_family X Tx D ∧ refine_of D A.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (regular_space_topology_on X Tx Hreg).
Set B to be the term {U ∈ Tx|∃a : set, a ∈ A ∧ closure_of X Tx U ⊆ a}.
We prove the intermediate claim HBop: ∀u : set, u ∈ B → u ∈ Tx.
Let u be given.
Assume HuB: u ∈ B.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃a0 : set, a0 ∈ A ∧ closure_of X Tx U0 ⊆ a0) u HuB).
We prove the intermediate claim HBcov: covers X B.
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃b : set, b ∈ B ∧ x ∈ b.
We prove the intermediate claim HAcovers: covers X A.
An exact proof term for the current goal is (open_cover_implies_covers X Tx A HAcov).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ x ∈ a.
An exact proof term for the current goal is (HAcovers x HxX).
Apply Hexa to the current goal.
Let a be given.
Assume Hapack: a ∈ A ∧ x ∈ a.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (x ∈ a) Hapack).
We prove the intermediate claim Hxa: x ∈ a.
An exact proof term for the current goal is (andER (a ∈ A) (x ∈ a) Hapack).
We prove the intermediate claim HaTx: a ∈ Tx.
An exact proof term for the current goal is (open_cover_members_open X Tx A a HAcov HaA).
We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ a.
An exact proof term for the current goal is (regular_space_shrink_neighborhood X Tx x a Hreg HxX HaTx Hxa).
Apply HexV to the current goal.
Let V be given.
Assume HVpack: V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ a.
We prove the intermediate claim HVpair: (V ∈ Tx ∧ x ∈ V).
An exact proof term for the current goal is (andEL (V ∈ Tx ∧ x ∈ V) (closure_of X Tx V ⊆ a) HVpack).
We prove the intermediate claim HVT: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (x ∈ V) HVpair).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (x ∈ V) HVpair).
We prove the intermediate claim HclVsuba: closure_of X Tx V ⊆ a.
An exact proof term for the current goal is (andER (V ∈ Tx ∧ x ∈ V) (closure_of X Tx V ⊆ a) HVpack).
We use V to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HVpred: ∃a0 : set, a0 ∈ A ∧ closure_of X Tx V ⊆ a0.
We use a to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HaA.
An exact proof term for the current goal is HclVsuba.
An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ ∃a0 : set, a0 ∈ A ∧ closure_of X Tx U0 ⊆ a0) V HVT HVpred).
An exact proof term for the current goal is HxV.
We prove the intermediate claim HBcover: open_cover X Tx B.
We will prove (∀u : set, u ∈ B → u ∈ Tx) ∧ covers X B.
Apply andI to the current goal.
An exact proof term for the current goal is HBop.
An exact proof term for the current goal is HBcov.
We prove the intermediate claim HexC: ∃C : set, covers X C ∧ locally_finite_family X Tx C ∧ refine_of C B.
An exact proof term for the current goal is (Hcond2 B HBcover).
Apply HexC to the current goal.
Let C be given.
Assume HCpack: covers X C ∧ locally_finite_family X Tx C ∧ refine_of C B.
We prove the intermediate claim HCcovlf: covers X C ∧ locally_finite_family X Tx C.
An exact proof term for the current goal is (andEL (covers X C ∧ locally_finite_family X Tx C) (refine_of C B) HCpack).
We prove the intermediate claim HcovC: covers X C.
An exact proof term for the current goal is (andEL (covers X C) (locally_finite_family X Tx C) HCcovlf).
We prove the intermediate claim HlfC: locally_finite_family X Tx C.
An exact proof term for the current goal is (andER (covers X C) (locally_finite_family X Tx C) HCcovlf).
We prove the intermediate claim HrefCB: refine_of C B.
An exact proof term for the current goal is (andER (covers X C ∧ locally_finite_family X Tx C) (refine_of C B) HCpack).
Set D to be the term {closure_of X Tx c|c ∈ C}.
We use D to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove closed_cover X Tx D.
We will prove (∀d : set, d ∈ D → closed_in X Tx d) ∧ covers X D.
Apply andI to the current goal.
Let d be given.
Assume HdD: d ∈ D.
We will prove closed_in X Tx d.
Apply (ReplE_impred C (λc0 : set ⇒ closure_of X Tx c0) d HdD) to the current goal.
Let c be given.
Assume HcC: c ∈ C.
Assume Hdeq: d = closure_of X Tx c.
We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ c ⊆ b.
An exact proof term for the current goal is (HrefCB c HcC).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack: b ∈ B ∧ c ⊆ b.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (c ⊆ b) Hbpack).
We prove the intermediate claim Hcsubb: c ⊆ b.
An exact proof term for the current goal is (andER (b ∈ B) (c ⊆ b) Hbpack).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃a0 : set, a0 ∈ A ∧ closure_of X Tx U0 ⊆ a0) b HbB).
We prove the intermediate claim HbPow: b ∈ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx b HbTx).
We prove the intermediate claim HbsubX: b ⊆ X.
Let z be given.
Assume Hz: z ∈ b.
An exact proof term for the current goal is (PowerE X b HbPow z Hz).
We prove the intermediate claim HcsubX: c ⊆ X.
An exact proof term for the current goal is (Subq_tra c b X Hcsubb HbsubX).
rewrite the current goal using Hdeq (from left to right).
An exact proof term for the current goal is (closure_is_closed X Tx c HTx HcsubX).
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃d : set, d ∈ D ∧ x ∈ d.
We prove the intermediate claim Hexc: ∃c : set, c ∈ C ∧ x ∈ c.
An exact proof term for the current goal is (HcovC x HxX).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpack: c ∈ C ∧ x ∈ c.
We prove the intermediate claim HcC: c ∈ C.
An exact proof term for the current goal is (andEL (c ∈ C) (x ∈ c) Hcpack).
We prove the intermediate claim Hxc: x ∈ c.
An exact proof term for the current goal is (andER (c ∈ C) (x ∈ c) Hcpack).
We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ c ⊆ b.
An exact proof term for the current goal is (HrefCB c HcC).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack: b ∈ B ∧ c ⊆ b.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (c ⊆ b) Hbpack).
We prove the intermediate claim Hcsubb: c ⊆ b.
An exact proof term for the current goal is (andER (b ∈ B) (c ⊆ b) Hbpack).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃a0 : set, a0 ∈ A ∧ closure_of X Tx U0 ⊆ a0) b HbB).
We prove the intermediate claim HbPow: b ∈ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx b HbTx).
We prove the intermediate claim HbsubX: b ⊆ X.
Let z be given.
Assume Hz: z ∈ b.
An exact proof term for the current goal is (PowerE X b HbPow z Hz).
We prove the intermediate claim HcsubX: c ⊆ X.
An exact proof term for the current goal is (Subq_tra c b X Hcsubb HbsubX).
We use (closure_of X Tx c) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI C (λc0 : set ⇒ closure_of X Tx c0) c HcC).
We prove the intermediate claim Hcsubcl: c ⊆ closure_of X Tx c.
An exact proof term for the current goal is (closure_contains_set X Tx c HTx HcsubX).
An exact proof term for the current goal is (Hcsubcl x Hxc).
An exact proof term for the current goal is (locally_finite_family_closure_image X Tx C HlfC).
Let d be given.
Assume HdD: d ∈ D.
We will prove ∃a : set, a ∈ A ∧ d ⊆ a.
Apply (ReplE_impred C (λc0 : set ⇒ closure_of X Tx c0) d HdD) to the current goal.
Let c be given.
Assume HcC: c ∈ C.
Assume Hdeq: d = closure_of X Tx c.
We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ c ⊆ b.
An exact proof term for the current goal is (HrefCB c HcC).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack: b ∈ B ∧ c ⊆ b.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (c ⊆ b) Hbpack).
We prove the intermediate claim Hcsubb: c ⊆ b.
An exact proof term for the current goal is (andER (b ∈ B) (c ⊆ b) Hbpack).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ closure_of X Tx b ⊆ a.
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ ∃a0 : set, a0 ∈ A ∧ closure_of X Tx U0 ⊆ a0) b HbB).
Apply Hexa to the current goal.
Let a be given.
Assume Hapack: a ∈ A ∧ closure_of X Tx b ⊆ a.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (closure_of X Tx b ⊆ a) Hapack).
We prove the intermediate claim Hclbsuba: closure_of X Tx b ⊆ a.
An exact proof term for the current goal is (andER (a ∈ A) (closure_of X Tx b ⊆ a) Hapack).
We use a to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HaA.
rewrite the current goal using Hdeq (from left to right).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃a0 : set, a0 ∈ A ∧ closure_of X Tx U0 ⊆ a0) b HbB).
We prove the intermediate claim HbPow: b ∈ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx b HbTx).
We prove the intermediate claim HbsubX: b ⊆ X.
Let z be given.
Assume Hz: z ∈ b.
An exact proof term for the current goal is (PowerE X b HbPow z Hz).
We prove the intermediate claim Hclcsubclb: closure_of X Tx c ⊆ closure_of X Tx b.
An exact proof term for the current goal is (closure_monotone X Tx c b HTx Hcsubb HbsubX).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx c) (closure_of X Tx b) a Hclcsubclb Hclbsuba).
∎