Let X, Tx and A be given.
Assume Hreg: regular_space X Tx.
Assume HA: open_cover X Tx A.
Assume Hcond3: Michael_cond41_3_3 X Tx.
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).
We prove the intermediate claim HexB: ∃B : set, closed_cover X Tx B ∧ locally_finite_family X Tx B ∧ refine_of B A.
An exact proof term for the current goal is (Hcond3 A HA).
Apply HexB to the current goal.
Let B be given.
Assume HB: closed_cover X Tx B ∧ locally_finite_family X Tx B ∧ refine_of B A.
We prove the intermediate claim HBcovlf: closed_cover X Tx B ∧ locally_finite_family X Tx B.
An exact proof term for the current goal is (andEL (closed_cover X Tx B ∧ locally_finite_family X Tx B) (refine_of B A) HB).
We prove the intermediate claim HBcovcl: closed_cover X Tx B.
An exact proof term for the current goal is (andEL (closed_cover X Tx B) (locally_finite_family X Tx B) HBcovlf).
We prove the intermediate claim HBlf: locally_finite_family X Tx B.
An exact proof term for the current goal is (andER (closed_cover X Tx B) (locally_finite_family X Tx B) HBcovlf).
We prove the intermediate claim HrefBA: refine_of B A.
An exact proof term for the current goal is (andER (closed_cover X Tx B ∧ locally_finite_family X Tx B) (refine_of B A) HB).
We prove the intermediate claim HBclosed: ∀b : set, b ∈ B → closed_in X Tx b.
An exact proof term for the current goal is (andEL (∀c : set, c ∈ B → closed_in X Tx c) (covers X B) HBcovcl).
We prove the intermediate claim HBcovers: covers X B.
An exact proof term for the current goal is (andER (∀c : set, c ∈ B → closed_in X Tx c) (covers X B) HBcovcl).
Set NbhdCover to be the term {N ∈ Tx|∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N ≠ Empty → b ∈ S}.
We prove the intermediate claim HNbhdOpenCover: open_cover X Tx NbhdCover.
We will prove (∀u : set, u ∈ NbhdCover → u ∈ Tx) ∧ covers X NbhdCover.
Apply andI to the current goal.
Let u be given.
Assume Hu: u ∈ NbhdCover.
An exact proof term for the current goal is (SepE1 Tx (λN0 : set ⇒ ∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N0 ≠ Empty → b ∈ S) u Hu).
We will prove covers X NbhdCover.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N ≠ Empty → b ∈ S.
An exact proof term for the current goal is (locally_finite_family_property X Tx B HBlf x HxX).
Apply HexN to the current goal.
Let N be given.
Assume HN: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N ≠ Empty → b ∈ S.
We use N to witness the existential quantifier.
Apply andI to the current goal.
We will prove N ∈ NbhdCover.
We prove the intermediate claim HNTx_xN: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N ≠ Empty → b ∈ S) HN).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HNTx_xN).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N ≠ Empty → b ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N ≠ Empty → b ∈ S) HN).
An exact proof term for the current goal is (SepI Tx (λN0 : set ⇒ ∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N0 ≠ Empty → b ∈ S) N HNTx HexS).
We prove the intermediate claim HNTx_xN: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N ≠ Empty → b ∈ S) HN).
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HNTx_xN).
We prove the intermediate claim HexC: ∃C : set, closed_cover X Tx C ∧ locally_finite_family X Tx C ∧ refine_of C NbhdCover.
An exact proof term for the current goal is (Hcond3 NbhdCover HNbhdOpenCover).
Apply HexC to the current goal.
Let C be given.
Assume HC: closed_cover X Tx C ∧ locally_finite_family X Tx C ∧ refine_of C NbhdCover.
We prove the intermediate claim HCcovlf: closed_cover X Tx C ∧ locally_finite_family X Tx C.
An exact proof term for the current goal is (andEL (closed_cover X Tx C ∧ locally_finite_family X Tx C) (refine_of C NbhdCover) HC).
We prove the intermediate claim HCcovcl: closed_cover X Tx C.
An exact proof term for the current goal is (andEL (closed_cover X Tx C) (locally_finite_family X Tx C) HCcovlf).
We prove the intermediate claim HClf: locally_finite_family X Tx C.
An exact proof term for the current goal is (andER (closed_cover X Tx C) (locally_finite_family X Tx C) HCcovlf).
We prove the intermediate claim HrefCN: refine_of C NbhdCover.
An exact proof term for the current goal is (andER (closed_cover X Tx C ∧ locally_finite_family X Tx C) (refine_of C NbhdCover) HC).
We prove the intermediate claim HCclosed: ∀c : set, c ∈ C → closed_in X Tx c.
An exact proof term for the current goal is (andEL (∀c0 : set, c0 ∈ C → closed_in X Tx c0) (covers X C) HCcovcl).
We prove the intermediate claim HCcovers: covers X C.
An exact proof term for the current goal is (andER (∀c0 : set, c0 ∈ C → closed_in X Tx c0) (covers X C) HCcovcl).
Set Fpick to be the term λb : set ⇒ Eps_i (λa : set ⇒ a ∈ A ∧ b ⊆ a).
Set C_of to be the term λb : set ⇒ {c ∈ C|c ⊆ X ∖ b}.
Set E_of to be the term λb : set ⇒ X ∖ ⋃ (C_of b).
Set D to be the term {(E_of b) ∩ (Fpick b)|b ∈ B}.
We prove the intermediate claim HE_open: ∀b : set, b ∈ B → (E_of b) ∈ Tx.
Let b be given.
Assume HbB: b ∈ B.
Set CB to be the term C_of b.
We prove the intermediate claim HCBsub: CB ⊆ C.
Let c be given.
Assume Hc: c ∈ CB.
An exact proof term for the current goal is (SepE1 C (λc0 : set ⇒ c0 ⊆ X ∖ b) c Hc).
We prove the intermediate claim HUnionCBclosed: closed_in X Tx (⋃ CB).
Apply (Union_subfamily_locally_finite_closed_is_closed X Tx C CB HClf HCclosed HCBsub) to the current goal.
We prove the intermediate claim Hop: open_in X Tx (X ∖ (⋃ CB)).
An exact proof term for the current goal is (open_of_closed_complement X Tx (⋃ CB) HUnionCBclosed).
We prove the intermediate claim HopElem: (X ∖ (⋃ CB)) ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ (⋃ CB)) Hop).
An exact proof term for the current goal is HopElem.
We prove the intermediate claim HBsubE: ∀b : set, b ∈ B → b ⊆ E_of b.
Let b be given.
Assume HbB: b ∈ B.
Set CB to be the term C_of b.
We prove the intermediate claim HcSubX: ∀c : set, c ∈ C → c ⊆ X.
Let c be given.
Assume HcC: c ∈ C.
We prove the intermediate claim HcCl: closed_in X Tx c.
An exact proof term for the current goal is (HCclosed c HcC).
We prove the intermediate claim HcAnd: c ⊆ X ∧ ∃U ∈ Tx, c = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (c ⊆ X ∧ ∃U ∈ Tx, c = X ∖ U) HcCl).
An exact proof term for the current goal is (andEL (c ⊆ X) (∃U ∈ Tx, c = X ∖ U) HcAnd).
We prove the intermediate claim HbsubX: b ⊆ X.
We prove the intermediate claim HbCl: closed_in X Tx b.
An exact proof term for the current goal is (HBclosed b HbB).
We prove the intermediate claim HbAnd: b ⊆ X ∧ ∃U ∈ Tx, b = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (b ⊆ X ∧ ∃U ∈ Tx, b = X ∖ U) HbCl).
An exact proof term for the current goal is (andEL (b ⊆ X) (∃U ∈ Tx, b = X ∖ U) HbAnd).
Let x be given.
Assume HxB: x ∈ b.
We will prove x ∈ E_of b.
We prove the intermediate claim HEeq: E_of b = X ∖ ⋃ CB.
Use reflexivity.
rewrite the current goal using HEeq (from left to right).
Apply setminusI to the current goal.
An exact proof term for the current goal is (HbsubX x HxB).
Assume HxU: x ∈ ⋃ CB.
Apply (UnionE_impred CB x HxU False) to the current goal.
Let c be given.
Assume Hxc: x ∈ c.
Assume HcCB: c ∈ CB.
We prove the intermediate claim HcC: c ∈ C.
An exact proof term for the current goal is (SepE1 C (λc0 : set ⇒ c0 ⊆ X ∖ b) c HcCB).
We prove the intermediate claim Hcsub: c ⊆ X ∖ b.
An exact proof term for the current goal is (SepE2 C (λc0 : set ⇒ c0 ⊆ X ∖ b) c HcCB).
We prove the intermediate claim HxNotb: x ∉ b.
We prove the intermediate claim HxInComp: x ∈ X ∖ b.
An exact proof term for the current goal is (Hcsub x Hxc).
An exact proof term for the current goal is (setminusE2 X b x HxInComp).
An exact proof term for the current goal is (HxNotb HxB).
We prove the intermediate claim HFpickA: ∀b : set, b ∈ B → (Fpick b) ∈ A ∧ b ⊆ (Fpick b).
Let b be given.
Assume HbB: b ∈ B.
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ b ⊆ a.
An exact proof term for the current goal is (HrefBA b HbB).
An exact proof term for the current goal is (Eps_i_ex (λa : set ⇒ a ∈ A ∧ b ⊆ a) Hexa).
We prove the intermediate claim HFpickOpen: ∀b : set, b ∈ B → (Fpick b) ∈ Tx.
Let b be given.
Assume HbB: b ∈ B.
We prove the intermediate claim Hpack: (Fpick b) ∈ A ∧ b ⊆ (Fpick b).
An exact proof term for the current goal is (HFpickA b HbB).
We prove the intermediate claim HFinA: (Fpick b) ∈ A.
An exact proof term for the current goal is (andEL ((Fpick b) ∈ A) (b ⊆ (Fpick b)) Hpack).
An exact proof term for the current goal is (open_cover_members_open X Tx A (Fpick b) HA HFinA).
We prove the intermediate claim HDopen: ∀d : set, d ∈ D → d ∈ Tx.
Let d be given.
Assume HdD: d ∈ D.
Apply (ReplE_impred B (λb0 : set ⇒ (E_of b0) ∩ (Fpick b0)) d HdD (d ∈ Tx)) to the current goal.
Let b0 be given.
Assume Hb0: b0 ∈ B.
Assume Hdeq: d = (E_of b0) ∩ (Fpick b0).
We prove the intermediate claim HE: (E_of b0) ∈ Tx.
An exact proof term for the current goal is (HE_open b0 Hb0).
We prove the intermediate claim HF: (Fpick b0) ∈ Tx.
An exact proof term for the current goal is (HFpickOpen b0 Hb0).
rewrite the current goal using Hdeq (from left to right).
An exact proof term for the current goal is (topology_binintersect_axiom X Tx HTx (E_of b0) HE (Fpick b0) HF).
We prove the intermediate claim HDref: refine_of D A.
Let d be given.
Assume HdD: d ∈ D.
Apply (ReplE_impred B (λb0 : set ⇒ (E_of b0) ∩ (Fpick b0)) d HdD (∃a : set, a ∈ A ∧ d ⊆ a)) to the current goal.
Let b0 be given.
Assume Hb0: b0 ∈ B.
Assume Hdeq: d = (E_of b0) ∩ (Fpick b0).
We prove the intermediate claim Hpack: (Fpick b0) ∈ A ∧ b0 ⊆ (Fpick b0).
An exact proof term for the current goal is (HFpickA b0 Hb0).
We prove the intermediate claim HaA: (Fpick b0) ∈ A.
An exact proof term for the current goal is (andEL ((Fpick b0) ∈ A) (b0 ⊆ (Fpick b0)) Hpack).
We use (Fpick b0) 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).
An exact proof term for the current goal is (binintersect_Subq_2 (E_of b0) (Fpick b0)).
We prove the intermediate claim HDcov: covers X D.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ x ∈ b.
Apply (HBcovers x HxX) to the current goal.
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack: b ∈ B ∧ x ∈ b.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b) Hbpack).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b) Hbpack).
We use ((E_of b) ∩ (Fpick b)) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI B (λb0 : set ⇒ (E_of b0) ∩ (Fpick b0)) b HbB).
Apply binintersectI to the current goal.
An exact proof term for the current goal is (HBsubE b HbB x Hxb).
We prove the intermediate claim Hpack: (Fpick b) ∈ A ∧ b ⊆ (Fpick b).
An exact proof term for the current goal is (HFpickA b HbB).
We prove the intermediate claim HbsubF: b ⊆ (Fpick b).
An exact proof term for the current goal is (andER ((Fpick b) ∈ A) (b ⊆ (Fpick b)) Hpack).
An exact proof term for the current goal is (HbsubF x Hxb).
We prove the intermediate claim HDopenCover: open_cover X Tx D.
We will prove (∀u : set, u ∈ D → u ∈ Tx) ∧ covers X D.
Apply andI to the current goal.
An exact proof term for the current goal is HDopen.
An exact proof term for the current goal is HDcov.
We prove the intermediate claim HClfProp: ∀c : set, c ∈ C → ∃S0 : set, finite S0 ∧ S0 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c ≠ Empty → b ∈ S0.
Let c be given.
Assume HcC: c ∈ C.
We prove the intermediate claim HexU: ∃U : set, U ∈ NbhdCover ∧ c ⊆ U.
An exact proof term for the current goal is (HrefCN c HcC).
Apply HexU to the current goal.
Let U be given.
Assume HUpack: U ∈ NbhdCover ∧ c ⊆ U.
We prove the intermediate claim HUcov: U ∈ NbhdCover.
An exact proof term for the current goal is (andEL (U ∈ NbhdCover) (c ⊆ U) HUpack).
We prove the intermediate claim HcsubU: c ⊆ U.
An exact proof term for the current goal is (andER (U ∈ NbhdCover) (c ⊆ U) HUpack).
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λN0 : set ⇒ ∃S : set, finite S ∧ S ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N0 ≠ Empty → b ∈ S) U HUcov).
We prove the intermediate claim HexS0: ∃S0 : set, finite S0 ∧ S0 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ U ≠ Empty → b ∈ S0.
An exact proof term for the current goal is (SepE2 Tx (λN0 : set ⇒ ∃S0 : set, finite S0 ∧ S0 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ N0 ≠ Empty → b ∈ S0) U HUcov).
Apply HexS0 to the current goal.
Let S0 be given.
Assume HS0: finite S0 ∧ S0 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ U ≠ Empty → b ∈ S0.
We use S0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (finite S0) (S0 ⊆ B) (andEL (finite S0 ∧ S0 ⊆ B) (∀b : set, b ∈ B → b ∩ U ≠ Empty → b ∈ S0) HS0)).
An exact proof term for the current goal is (andER (finite S0) (S0 ⊆ B) (andEL (finite S0 ∧ S0 ⊆ B) (∀b : set, b ∈ B → b ∩ U ≠ Empty → b ∈ S0) HS0)).
Let b be given.
Assume HbB: b ∈ B.
Assume HbIntC: b ∩ c ≠ Empty.
We prove the intermediate claim HbIntU: b ∩ U ≠ Empty.
Assume HbEmp: b ∩ U = Empty.
We prove the intermediate claim Hexz: ∃z : set, z ∈ b ∩ c.
An exact proof term for the current goal is (nonempty_has_element (b ∩ c) HbIntC).
Apply Hexz to the current goal.
Let z be given.
Assume Hz: z ∈ b ∩ c.
We prove the intermediate claim Hzb: z ∈ b.
An exact proof term for the current goal is (binintersectE1 b c z Hz).
We prove the intermediate claim Hzc: z ∈ c.
An exact proof term for the current goal is (binintersectE2 b c z Hz).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HcsubU z Hzc).
We prove the intermediate claim HzIntU: z ∈ b ∩ U.
An exact proof term for the current goal is (binintersectI b U z Hzb HzU).
We prove the intermediate claim HzEmpty: z ∈ Empty.
rewrite the current goal using HbEmp (from right to left).
An exact proof term for the current goal is HzIntU.
An exact proof term for the current goal is (EmptyE z HzEmpty False).
We prove the intermediate claim HSprop: ∀b0 : set, b0 ∈ B → b0 ∩ U ≠ Empty → b0 ∈ S0.
An exact proof term for the current goal is (andER (finite S0 ∧ S0 ⊆ B) (∀b0 : set, b0 ∈ B → b0 ∩ U ≠ Empty → b0 ∈ S0) HS0).
An exact proof term for the current goal is (HSprop b HbB HbIntU).
We use D to witness the existential quantifier.
Apply andI to the current goal.
We will prove open_cover X Tx D ∧ locally_finite_family X Tx D.
Apply andI to the current goal.
An exact proof term for the current goal is HDopenCover.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S0 : set, finite S0 ∧ S0 ⊆ D ∧ ∀d : set, d ∈ D → d ∩ N ≠ Empty → d ∈ S0.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃SC : set, finite SC ∧ SC ⊆ C ∧ ∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC.
An exact proof term for the current goal is (locally_finite_family_property X Tx C HClf x HxX).
Apply HexN to the current goal.
Let N be given.
Assume HN: N ∈ Tx ∧ x ∈ N ∧ ∃SC : set, finite SC ∧ SC ⊆ C ∧ ∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC.
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) (∃SC : set, finite SC ∧ SC ⊆ C ∧ ∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC) HN).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HNpair).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HNpair).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HNTx.
An exact proof term for the current goal is HxN.
We prove the intermediate claim HexSC: ∃SC : set, finite SC ∧ SC ⊆ C ∧ ∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃SC : set, finite SC ∧ SC ⊆ C ∧ ∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC) HN).
Apply HexSC to the current goal.
Let SC be given.
Assume HSC: finite SC ∧ SC ⊆ C ∧ ∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC.
We prove the intermediate claim HSCfin: finite SC.
An exact proof term for the current goal is (andEL (finite SC) (SC ⊆ C) (andEL (finite SC ∧ SC ⊆ C) (∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC) HSC)).
We prove the intermediate claim HSCsubC: SC ⊆ C.
An exact proof term for the current goal is (andER (finite SC) (SC ⊆ C) (andEL (finite SC ∧ SC ⊆ C) (∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC) HSC)).
We prove the intermediate claim HSCprop: ∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC.
An exact proof term for the current goal is (andER (finite SC ∧ SC ⊆ C) (∀c : set, c ∈ C → c ∩ N ≠ Empty → c ∈ SC) HSC).
Set Bpick to be the term λc : set ⇒ Eps_i (λS0 : set ⇒ finite S0 ∧ S0 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c ≠ Empty → b ∈ S0).
Set BFam to be the term {Bpick c|c ∈ SC}.
Set Bfin to be the term ⋃ BFam.
Set Dfin to be the term {(E_of b) ∩ (Fpick b)|b ∈ Bfin}.
We prove the intermediate claim HBFamFin: finite BFam.
An exact proof term for the current goal is (finite_Repl SC HSCfin (λc0 : set ⇒ Bpick c0)).
We prove the intermediate claim HBFamAllFin: ∀S0 : set, S0 ∈ BFam → finite S0.
Let S0 be given.
Assume HS0: S0 ∈ BFam.
Apply (ReplE_impred SC (λc0 : set ⇒ Bpick c0) S0 HS0 (finite S0)) to the current goal.
Let c0 be given.
Assume Hc0: c0 ∈ SC.
Assume HS0eq: S0 = Bpick c0.
We prove the intermediate claim Hc0C: c0 ∈ C.
An exact proof term for the current goal is (HSCsubC c0 Hc0).
We prove the intermediate claim HexS0: ∃S1 : set, finite S1 ∧ S1 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c0 ≠ Empty → b ∈ S1.
An exact proof term for the current goal is (HClfProp c0 Hc0C).
We prove the intermediate claim HS0prop: finite (Bpick c0) ∧ (Bpick c0) ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c0 ≠ Empty → b ∈ (Bpick c0).
An exact proof term for the current goal is (Eps_i_ex (λS1 : set ⇒ finite S1 ∧ S1 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c0 ≠ Empty → b ∈ S1) HexS0).
rewrite the current goal using HS0eq (from left to right).
We prove the intermediate claim HS0left: finite (Bpick c0) ∧ (Bpick c0) ⊆ B.
An exact proof term for the current goal is (andEL (finite (Bpick c0) ∧ (Bpick c0) ⊆ B) (∀b : set, b ∈ B → b ∩ c0 ≠ Empty → b ∈ (Bpick c0)) HS0prop).
An exact proof term for the current goal is (andEL (finite (Bpick c0)) ((Bpick c0) ⊆ B) HS0left).
We prove the intermediate claim HBfinFin: finite Bfin.
An exact proof term for the current goal is (finite_Union_of_finite_family BFam HBFamFin HBFamAllFin).
We prove the intermediate claim HDfinFin: finite Dfin.
An exact proof term for the current goal is (finite_Repl Bfin HBfinFin (λb0 : set ⇒ (E_of b0) ∩ (Fpick b0))).
We prove the intermediate claim HBfinSubB: Bfin ⊆ B.
Let b0 be given.
Assume Hb0: b0 ∈ Bfin.
Apply (UnionE_impred BFam b0 Hb0 (b0 ∈ B)) to the current goal.
Let S0 be given.
Assume Hb0S0: b0 ∈ S0.
Assume HS0BFam: S0 ∈ BFam.
We prove the intermediate claim HS0subB: S0 ⊆ B.
Apply (ReplE_impred SC (λc0 : set ⇒ Bpick c0) S0 HS0BFam (S0 ⊆ B)) to the current goal.
Let c0 be given.
Assume Hc0: c0 ∈ SC.
Assume HS0eq: S0 = Bpick c0.
We prove the intermediate claim Hc0C: c0 ∈ C.
An exact proof term for the current goal is (HSCsubC c0 Hc0).
We prove the intermediate claim HexS0: ∃S1 : set, finite S1 ∧ S1 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c0 ≠ Empty → b ∈ S1.
An exact proof term for the current goal is (HClfProp c0 Hc0C).
We prove the intermediate claim HS0prop: finite (Bpick c0) ∧ (Bpick c0) ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c0 ≠ Empty → b ∈ (Bpick c0).
An exact proof term for the current goal is (Eps_i_ex (λS1 : set ⇒ finite S1 ∧ S1 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c0 ≠ Empty → b ∈ S1) HexS0).
We prove the intermediate claim HS0left: finite (Bpick c0) ∧ (Bpick c0) ⊆ B.
An exact proof term for the current goal is (andEL (finite (Bpick c0) ∧ (Bpick c0) ⊆ B) (∀b : set, b ∈ B → b ∩ c0 ≠ Empty → b ∈ (Bpick c0)) HS0prop).
rewrite the current goal using HS0eq (from left to right).
An exact proof term for the current goal is (andER (finite (Bpick c0)) ((Bpick c0) ⊆ B) HS0left).
An exact proof term for the current goal is (HS0subB b0 Hb0S0).
We prove the intermediate claim HDfinSubD: Dfin ⊆ D.
Let d0 be given.
Assume Hd0: d0 ∈ Dfin.
Apply (ReplE_impred Bfin (λb0 : set ⇒ (E_of b0) ∩ (Fpick b0)) d0 Hd0 (d0 ∈ D)) to the current goal.
Let b0 be given.
Assume Hb0: b0 ∈ Bfin.
Assume Hd0eq: d0 = (E_of b0) ∩ (Fpick b0).
We prove the intermediate claim Hb0B: b0 ∈ B.
An exact proof term for the current goal is (HBfinSubB b0 Hb0).
rewrite the current goal using Hd0eq (from left to right).
An exact proof term for the current goal is (ReplI B (λb1 : set ⇒ (E_of b1) ∩ (Fpick b1)) b0 Hb0B).
We use Dfin to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HDfinFin.
An exact proof term for the current goal is HDfinSubD.
Let d0 be given.
Assume Hd0D: d0 ∈ D.
Assume Hd0IntN: d0 ∩ N ≠ Empty.
We prove the intermediate claim Hexy: ∃y : set, y ∈ d0 ∩ N.
An exact proof term for the current goal is (nonempty_has_element (d0 ∩ N) Hd0IntN).
Apply Hexy to the current goal.
Let y be given.
Assume HyInt: y ∈ d0 ∩ N.
We prove the intermediate claim Hyd0: y ∈ d0.
An exact proof term for the current goal is (binintersectE1 d0 N y HyInt).
We prove the intermediate claim HyN: y ∈ N.
An exact proof term for the current goal is (binintersectE2 d0 N y HyInt).
Apply (ReplE_impred B (λb0 : set ⇒ (E_of b0) ∩ (Fpick b0)) d0 Hd0D (d0 ∈ Dfin)) to the current goal.
Let b0 be given.
Assume Hb0B: b0 ∈ B.
Assume Hd0eq: d0 = (E_of b0) ∩ (Fpick b0).
We prove the intermediate claim Hyd0pair: y ∈ (E_of b0) ∩ (Fpick b0).
rewrite the current goal using Hd0eq (from right to left).
An exact proof term for the current goal is Hyd0.
We prove the intermediate claim HyE: y ∈ E_of b0.
An exact proof term for the current goal is (binintersectE1 (E_of b0) (Fpick b0) y Hyd0pair).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (setminusE1 X (⋃ (C_of b0)) y HyE).
We prove the intermediate claim Hexc: ∃c : set, c ∈ C ∧ y ∈ c.
An exact proof term for the current goal is (HCcovers y HyX).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpack: c ∈ C ∧ y ∈ c.
We prove the intermediate claim HcC: c ∈ C.
An exact proof term for the current goal is (andEL (c ∈ C) (y ∈ c) Hcpack).
We prove the intermediate claim Hyc: y ∈ c.
An exact proof term for the current goal is (andER (c ∈ C) (y ∈ c) Hcpack).
We prove the intermediate claim HcIntN: c ∩ N ≠ Empty.
Assume HcEmp: c ∩ N = Empty.
We prove the intermediate claim HyIntcN: y ∈ c ∩ N.
An exact proof term for the current goal is (binintersectI c N y Hyc HyN).
We prove the intermediate claim HyEmpty: y ∈ Empty.
rewrite the current goal using HcEmp (from right to left).
An exact proof term for the current goal is HyIntcN.
An exact proof term for the current goal is (EmptyE y HyEmpty False).
We prove the intermediate claim HcSC: c ∈ SC.
An exact proof term for the current goal is (HSCprop c HcC HcIntN).
We prove the intermediate claim HBpickProp: finite (Bpick c) ∧ (Bpick c) ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c ≠ Empty → b ∈ (Bpick c).
We prove the intermediate claim HexS0: ∃S1 : set, finite S1 ∧ S1 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c ≠ Empty → b ∈ S1.
An exact proof term for the current goal is (HClfProp c HcC).
An exact proof term for the current goal is (Eps_i_ex (λS1 : set ⇒ finite S1 ∧ S1 ⊆ B ∧ ∀b : set, b ∈ B → b ∩ c ≠ Empty → b ∈ S1) HexS0).
We prove the intermediate claim Hb0InBFam: (Bpick c) ∈ BFam.
An exact proof term for the current goal is (ReplI SC (λc0 : set ⇒ Bpick c0) c HcSC).
We prove the intermediate claim Hb0IntC: b0 ∩ c ≠ Empty.
Assume Hb0Emp: b0 ∩ c = Empty.
We prove the intermediate claim HcsubComp: c ⊆ X ∖ b0.
Let z be given.
Assume Hz: z ∈ c.
We prove the intermediate claim HzX: z ∈ X.
We prove the intermediate claim HcCl: closed_in X Tx c.
An exact proof term for the current goal is (HCclosed c HcC).
We prove the intermediate claim HcAnd: c ⊆ X ∧ ∃U ∈ Tx, c = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (c ⊆ X ∧ ∃U ∈ Tx, c = X ∖ U) HcCl).
We prove the intermediate claim HcsubX: c ⊆ X.
An exact proof term for the current goal is (andEL (c ⊆ X) (∃U ∈ Tx, c = X ∖ U) HcAnd).
An exact proof term for the current goal is (HcsubX z Hz).
We prove the intermediate claim HzNotb0: z ∉ b0.
Assume Hzb0: z ∈ b0.
We prove the intermediate claim HzInt: z ∈ b0 ∩ c.
An exact proof term for the current goal is (binintersectI b0 c z Hzb0 Hz).
We prove the intermediate claim HzEmpty: z ∈ Empty.
rewrite the current goal using Hb0Emp (from right to left).
An exact proof term for the current goal is HzInt.
An exact proof term for the current goal is (EmptyE z HzEmpty False).
An exact proof term for the current goal is (setminusI X b0 z HzX HzNotb0).
We prove the intermediate claim HcInCB: c ∈ C_of b0.
An exact proof term for the current goal is (SepI C (λc0 : set ⇒ c0 ⊆ X ∖ b0) c HcC HcsubComp).
We prove the intermediate claim HyUCB: y ∈ ⋃ (C_of b0).
An exact proof term for the current goal is (UnionI (C_of b0) y c Hyc HcInCB).
We prove the intermediate claim HyNotUCB: y ∉ ⋃ (C_of b0).
An exact proof term for the current goal is (setminusE2 X (⋃ (C_of b0)) y HyE).
An exact proof term for the current goal is (HyNotUCB HyUCB).
We prove the intermediate claim Hb0InPick: b0 ∈ (Bpick c).
We prove the intermediate claim HBpickForall: ∀b : set, b ∈ B → b ∩ c ≠ Empty → b ∈ (Bpick c).
An exact proof term for the current goal is (andER (finite (Bpick c) ∧ (Bpick c) ⊆ B) (∀b : set, b ∈ B → b ∩ c ≠ Empty → b ∈ (Bpick c)) HBpickProp).
An exact proof term for the current goal is (HBpickForall b0 Hb0B Hb0IntC).
We prove the intermediate claim Hb0InUnion: b0 ∈ ⋃ BFam.
An exact proof term for the current goal is (UnionI BFam b0 (Bpick c) Hb0InPick Hb0InBFam).
rewrite the current goal using Hd0eq (from left to right).
An exact proof term for the current goal is (ReplI Bfin (λb1 : set ⇒ (E_of b1) ∩ (Fpick b1)) b0 Hb0InUnion).
An exact proof term for the current goal is HDref.
∎