Let X, Tx and W be given.
Assume Hnorm: normal_space X Tx.
Assume HWcov: open_cover X Tx W.
Assume HWlf: locally_finite_family X Tx W.
We will prove ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim HWTx: ∀w : set, w ∈ W → w ∈ Tx.
An exact proof term for the current goal is (andEL (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcov).
We prove the intermediate claim HWcovers: covers X W.
An exact proof term for the current goal is (andER (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcov).
We prove the intermediate claim HTsubPow: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HWsubPow: W ⊆ 𝒫 X.
An exact proof term for the current goal is (open_cover_family_sub X Tx W HTx HWcov).
We prove the intermediate claim HWsubX: ∀w : set, w ∈ W → w ⊆ X.
Let w be given.
Assume HwW: w ∈ W.
An exact proof term for the current goal is (PowerE X w (HWsubPow w HwW)).
We prove the intermediate claim HWpointFin: ∀x : set, x ∈ X → ∃S : set, finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → x ∈ A → A ∈ S.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (locally_finite_family_point_finite_ex X Tx W HWlf x HxX).
Apply (xm (finite W)) to the current goal.
Assume HWfin: finite W.
We prove the intermediate claim HexV: ∃V : set, open_cover X Tx V ∧ finite V ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (normal_space_finite_open_cover_shrinking X Tx W Hnorm HWcov HWfin).
Apply HexV to the current goal.
Let V be given.
Assume HV: open_cover X Tx V ∧ finite V ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
We prove the intermediate claim HVcov: open_cover X Tx V.
Apply (and4E (open_cover X Tx V) (finite V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hcov Hfin Hsub Hcl.
An exact proof term for the current goal is Hcov.
We prove the intermediate claim HVfin: finite V.
Apply (and4E (open_cover X Tx V) (finite V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hcov Hfin Hsub Hcl.
An exact proof term for the current goal is Hfin.
We prove the intermediate claim HVsubW: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w.
Apply (and4E (open_cover X Tx V) (finite V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hcov Hfin Hsub Hcl.
An exact proof term for the current goal is Hsub.
We prove the intermediate claim HVclW: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
Apply (and4E (open_cover X Tx V) (finite V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hcov Hfin Hsub Hcl.
An exact proof term for the current goal is Hcl.
We prove the intermediate claim HVlf: locally_finite_family X Tx V.
An exact proof term for the current goal is (finite_open_cover_locally_finite X Tx V HTx HVcov HVfin).
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HVcov.
An exact proof term for the current goal is HVlf.
An exact proof term for the current goal is HVsubW.
An exact proof term for the current goal is HVclW.
Assume HWnotfin: ¬ (finite W).
We prove the intermediate claim HexWO: ∃I : set, well_ordered_set I ∧ equip W I.
An exact proof term for the current goal is (well_ordering_theorem_equip W).
Apply HexWO to the current goal.
Let I be given.
Assume HI: well_ordered_set I ∧ equip W I.
We prove the intermediate claim HwoI: well_ordered_set I.
An exact proof term for the current goal is (andEL (well_ordered_set I) (equip W I) HI).
We prove the intermediate claim HequipWI: equip W I.
An exact proof term for the current goal is (andER (well_ordered_set I) (equip W I) HI).
Apply HequipWI to the current goal.
Let idx be given.
Assume Hbij: bij W I idx.
We prove the intermediate claim HidxI: ∀w : set, w ∈ W → idx w ∈ I.
Apply (bijE W I idx Hbij (∀w : set, w ∈ W → idx w ∈ I)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H1.
We prove the intermediate claim HidxSurj: ∀i : set, i ∈ I → ∃w : set, w ∈ W ∧ idx w = i.
Apply (bijE W I idx Hbij (∀i : set, i ∈ I → ∃w : set, w ∈ W ∧ idx w = i)) to the current goal.
Assume H1 H2 H3.
Let i be given.
Assume Hi: i ∈ I.
An exact proof term for the current goal is (H3 i Hi).
Set pickW to be the term λi : set ⇒ Eps_i (λw : set ⇒ w ∈ W ∧ idx w = i).
We prove the intermediate claim HpickW: ∀i : set, i ∈ I → pickW i ∈ W ∧ idx (pickW i) = i.
Let i be given.
Assume Hi: i ∈ I.
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ idx w = i.
An exact proof term for the current goal is (HidxSurj i Hi).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ idx w = i.
An exact proof term for the current goal is (Eps_i_ax (λw0 : set ⇒ w0 ∈ W ∧ idx w0 = i) w Hw).
We prove the intermediate claim HidxInj: ∀u v : set, u ∈ W → v ∈ W → idx u = idx v → u = v.
Apply (bijE W I idx Hbij (∀u v : set, u ∈ W → v ∈ W → idx u = idx v → u = v)) to the current goal.
Assume H1 H2 H3.
Let u and v be given.
Assume Hu: u ∈ W.
Assume Hv: v ∈ W.
An exact proof term for the current goal is (H2 u Hu v Hv).
We prove the intermediate claim HpickW_idx: ∀w : set, w ∈ W → pickW (idx w) = w.
Let w be given.
Assume HwW: w ∈ W.
We prove the intermediate claim Hi: idx w ∈ I.
An exact proof term for the current goal is (HidxI w HwW).
We prove the intermediate claim Hpick: pickW (idx w) ∈ W ∧ idx (pickW (idx w)) = idx w.
An exact proof term for the current goal is (HpickW (idx w) Hi).
We prove the intermediate claim HpwW: pickW (idx w) ∈ W.
An exact proof term for the current goal is (andEL (pickW (idx w) ∈ W) (idx (pickW (idx w)) = idx w) Hpick).
We prove the intermediate claim HidxEq: idx (pickW (idx w)) = idx w.
An exact proof term for the current goal is (andER (pickW (idx w) ∈ W) (idx (pickW (idx w)) = idx w) Hpick).
An exact proof term for the current goal is (HidxInj (pickW (idx w)) w HpwW HwW HidxEq).
We prove the intermediate claim HexClW: ∃ClW : set, ClW = {closure_of X Tx w|w ∈ W} ∧ ((∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW) ∧ locally_finite_family X Tx ClW ∧ (∀C : set, C ∈ ClW → ∃w : set, w ∈ W ∧ C = closure_of X Tx w).
An exact proof term for the current goal is (locally_finite_open_cover_closures_closed_cover X Tx W HWcov HWlf).
Apply HexClW to the current goal.
Let ClW be given.
Assume HClWpack: ClW = {closure_of X Tx w|w ∈ W} ∧ ((∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW) ∧ locally_finite_family X Tx ClW ∧ (∀C : set, C ∈ ClW → ∃w : set, w ∈ W ∧ C = closure_of X Tx w).
We prove the intermediate claim HClWcore: (ClW = {closure_of X Tx w|w ∈ W} ∧ ((∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW)) ∧ locally_finite_family X Tx ClW.
An exact proof term for the current goal is (andEL ((ClW = {closure_of X Tx w|w ∈ W} ∧ ((∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW)) ∧ locally_finite_family X Tx ClW) (∀C : set, C ∈ ClW → ∃w : set, w ∈ W ∧ C = closure_of X Tx w) HClWpack).
We prove the intermediate claim HClWlf: locally_finite_family X Tx ClW.
An exact proof term for the current goal is (andER (ClW = {closure_of X Tx w|w ∈ W} ∧ ((∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW)) (locally_finite_family X Tx ClW) HClWcore).
We prove the intermediate claim HClWab: ClW = {closure_of X Tx w|w ∈ W} ∧ ((∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW).
An exact proof term for the current goal is (andEL (ClW = {closure_of X Tx w|w ∈ W} ∧ ((∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW)) (locally_finite_family X Tx ClW) HClWcore).
We prove the intermediate claim HClWclosedcov: (∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW.
An exact proof term for the current goal is (andER (ClW = {closure_of X Tx w|w ∈ W}) ((∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW) HClWab).
We prove the intermediate claim HClWclosed: ∀C : set, C ∈ ClW → closed_in X Tx C.
An exact proof term for the current goal is (andEL (∀C : set, C ∈ ClW → closed_in X Tx C) (covers X ClW) HClWclosedcov).
We prove the intermediate claim HClWcovers: covers X ClW.
An exact proof term for the current goal is (andER (∀C : set, C ∈ ClW → closed_in X Tx C) (covers X ClW) HClWclosedcov).
We prove the intermediate claim HWclosure_point_finite: ∀x : set, x ∈ X → ∃S : set, finite S ∧ S ⊆ W ∧ ∀w : set, w ∈ W → x ∈ closure_of X Tx w → w ∈ S.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (locally_finite_open_cover_closure_point_finite X Tx W x HWcov HWlf HxX).
We prove the intermediate claim HWneighborhood_strong_finite_subcover: ∀x : set, x ∈ X → ∃N S : set, N ∈ Tx ∧ x ∈ N ∧ finite S ∧ S ⊆ W ∧ N ⊆ ⋃ S.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (locally_finite_open_cover_neighborhood_finite_subunion X Tx W x HWcov HWlf HxX).
We prove the intermediate claim HexB: ∃B : set, (∀b : set, b ∈ B → b ∈ Tx) ∧ locally_finite_family X Tx B ∧ (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w) ∧ ∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ closure_of X Tx b ⊆ w.
An exact proof term for the current goal is (locally_finite_open_cover_core_family X Tx W HTx HWcov HWlf).
Apply HexB to the current goal.
Let B be given.
Assume HBpack.
We prove the intermediate claim HBABC: ((∀b : set, b ∈ B → b ∈ Tx) ∧ locally_finite_family X Tx B) ∧ (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w).
An exact proof term for the current goal is (andEL (((∀b : set, b ∈ B → b ∈ Tx) ∧ locally_finite_family X Tx B) ∧ (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w)) (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ closure_of X Tx b ⊆ w) HBpack).
We prove the intermediate claim HBclsubW: ∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ closure_of X Tx b ⊆ w.
An exact proof term for the current goal is (andER (((∀b : set, b ∈ B → b ∈ Tx) ∧ locally_finite_family X Tx B) ∧ (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w)) (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ closure_of X Tx b ⊆ w) HBpack).
We prove the intermediate claim HBAB: (∀b : set, b ∈ B → b ∈ Tx) ∧ locally_finite_family X Tx B.
An exact proof term for the current goal is (andEL ((∀b : set, b ∈ B → b ∈ Tx) ∧ locally_finite_family X Tx B) (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w) HBABC).
We prove the intermediate claim HBsubW: ∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w.
An exact proof term for the current goal is (andER ((∀b : set, b ∈ B → b ∈ Tx) ∧ locally_finite_family X Tx B) (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w) HBABC).
We prove the intermediate claim HBmemTx: ∀b : set, b ∈ B → b ∈ Tx.
An exact proof term for the current goal is (andEL (∀b : set, b ∈ B → b ∈ Tx) (locally_finite_family X Tx B) HBAB).
We prove the intermediate claim HBlf: locally_finite_family X Tx B.
An exact proof term for the current goal is (andER (∀b : set, b ∈ B → b ∈ Tx) (locally_finite_family X Tx B) HBAB).
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (normal_space_implies_regular X Tx Hnorm).
Set Wof to be the term (λi : set ⇒ pickW i).
Set Wlt to be the term (λi : set ⇒ {Wof j|j ∈ i}).
Set Ult to be the term (λi : set ⇒ ⋃ (Wlt i)).
We prove the intermediate claim HWofW: ∀i : set, i ∈ I → Wof i ∈ W.
Let i be given.
Assume Hi: i ∈ I.
An exact proof term for the current goal is (andEL (pickW i ∈ W) (idx (pickW i) = i) (HpickW i Hi)).
We prove the intermediate claim HWofSurj: ∀w : set, w ∈ W → ∃i : set, i ∈ I ∧ Wof i = w.
Let w be given.
Assume HwW: w ∈ W.
We use (idx w) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HidxI w HwW).
We prove the intermediate claim HWdef: Wof (idx w) = pickW (idx w).
Use reflexivity.
rewrite the current goal using HWdef (from left to right).
An exact proof term for the current goal is (HpickW_idx w HwW).
Set Wimg to be the term {Wof i|i ∈ I}.
We prove the intermediate claim HWimgEq: Wimg = W.
Apply set_ext to the current goal.
Let w be given.
Assume Hw: w ∈ Wimg.
We will prove w ∈ W.
Apply (ReplE_impred I (λi0 : set ⇒ Wof i0) w Hw (w ∈ W)) to the current goal.
Let i be given.
Assume Hi: i ∈ I.
Assume Heq: w = Wof i.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (HWofW i Hi).
Let w be given.
Assume HwW: w ∈ W.
We will prove w ∈ Wimg.
Apply HWofSurj w HwW to the current goal.
Let i be given.
Assume Hipair: i ∈ I ∧ Wof i = w.
We prove the intermediate claim Hi: i ∈ I.
An exact proof term for the current goal is (andEL (i ∈ I) (Wof i = w) Hipair).
We prove the intermediate claim Heq: Wof i = w.
An exact proof term for the current goal is (andER (i ∈ I) (Wof i = w) Hipair).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is (ReplI I (λi0 : set ⇒ Wof i0) i Hi).
We prove the intermediate claim HWofCovers: ∀x : set, x ∈ X → ∃i : set, i ∈ I ∧ x ∈ Wof i.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ x ∈ w.
An exact proof term for the current goal is (HWcovers x HxX).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ x ∈ w.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (x ∈ w) Hw).
We prove the intermediate claim Hxw: x ∈ w.
An exact proof term for the current goal is (andER (w ∈ W) (x ∈ w) Hw).
We prove the intermediate claim HwWimg: w ∈ Wimg.
rewrite the current goal using HWimgEq (from left to right).
An exact proof term for the current goal is HwW.
Apply (ReplE_impred I (λi0 : set ⇒ Wof i0) w HwWimg (∃i : set, i ∈ I ∧ x ∈ Wof i)) to the current goal.
Let i be given.
Assume Hi: i ∈ I.
Assume Heq: w = Wof i.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hxw.
We prove the intermediate claim HordI: ordinal I.
An exact proof term for the current goal is (well_ordered_set_is_ordinal I HwoI).
We prove the intermediate claim HTransI: TransSet I.
An exact proof term for the current goal is (ordinal_TransSet I HordI).
We prove the intermediate claim HWltSubW: ∀i : set, i ∈ I → Wlt i ⊆ W.
Let i be given.
Assume Hi: i ∈ I.
Let w be given.
Assume Hw: w ∈ Wlt i.
Apply (ReplE_impred i (λj : set ⇒ Wof j) w Hw (w ∈ W)) to the current goal.
Let j be given.
Assume Hj: j ∈ i.
Assume Heq: w = Wof j.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HisubI: i ⊆ I.
An exact proof term for the current goal is (HTransI i Hi).
We prove the intermediate claim HjI: j ∈ I.
An exact proof term for the current goal is (HisubI j Hj).
An exact proof term for the current goal is (HWofW j HjI).
We prove the intermediate claim HWltLF: ∀i : set, i ∈ I → locally_finite_family X Tx (Wlt i).
Let i be given.
Assume Hi: i ∈ I.
An exact proof term for the current goal is (locally_finite_subfamily X Tx W (Wlt i) HWlf (HWltSubW i Hi)).
We prove the intermediate claim HWltPowTx: ∀i : set, i ∈ I → Wlt i ∈ 𝒫 Tx.
Let i be given.
Assume Hi: i ∈ I.
Apply PowerI to the current goal.
Let w be given.
Assume Hw: w ∈ Wlt i.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (HWltSubW i Hi w Hw).
We prove the intermediate claim Hexj: ∃j : set, j ∈ i ∧ w = Wof j.
An exact proof term for the current goal is (ReplE i (λj0 : set ⇒ Wof j0) w Hw).
Apply Hexj to the current goal.
Let j be given.
Assume Hjpair: j ∈ i ∧ w = Wof j.
We prove the intermediate claim Hj: j ∈ i.
An exact proof term for the current goal is (andEL (j ∈ i) (w = Wof j) Hjpair).
We prove the intermediate claim Heq: w = Wof j.
An exact proof term for the current goal is (andER (j ∈ i) (w = Wof j) Hjpair).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HisubI: i ⊆ I.
An exact proof term for the current goal is (HTransI i Hi).
We prove the intermediate claim HjI: j ∈ I.
An exact proof term for the current goal is (HisubI j Hj).
We prove the intermediate claim HwjW: Wof j ∈ W.
An exact proof term for the current goal is (HWofW j HjI).
An exact proof term for the current goal is (HWTx (Wof j) HwjW).
We prove the intermediate claim HUltTx: ∀i : set, i ∈ I → Ult i ∈ Tx.
Let i be given.
Assume Hi: i ∈ I.
An exact proof term for the current goal is (topology_union_axiom X Tx HTx (Wlt i) (HWltPowTx i Hi)).
We prove the intermediate claim HUltSubU: ∀i : set, i ∈ I → Ult i ⊆ ⋃ W.
Let i be given.
Assume Hi: i ∈ I.
Let x be given.
Assume Hx: x ∈ Ult i.
Apply (UnionE_impred (Wlt i) x Hx) to the current goal.
Let w be given.
Assume Hxw: x ∈ w.
Assume Hw: w ∈ Wlt i.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (HWltSubW i Hi w Hw).
An exact proof term for the current goal is (UnionI W x w Hxw HwW).
Set Igt to be the term (λi : set ⇒ {j ∈ I|i ∈ j}).
Set Wgt to be the term (λi : set ⇒ {Wof j|j ∈ (Igt i)}).
Set LaterU to be the term (λi : set ⇒ ⋃ (Wgt i)).
We prove the intermediate claim HWofTx: ∀i : set, i ∈ I → Wof i ∈ Tx.
Let i be given.
Assume Hi: i ∈ I.
An exact proof term for the current goal is (HWTx (Wof i) (HWofW i Hi)).
We prove the intermediate claim HWgtPowTx: ∀i : set, i ∈ I → Wgt i ∈ 𝒫 Tx.
Let i be given.
Assume Hi: i ∈ I.
Apply PowerI to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Wgt i.
Apply (ReplE_impred (Igt i) (λj : set ⇒ Wof j) U0 HU0 (U0 ∈ Tx)) to the current goal.
Let j be given.
Assume Hj: j ∈ Igt i.
Assume Heq: U0 = Wof j.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HjI: j ∈ I.
An exact proof term for the current goal is (SepE1 I (λj0 : set ⇒ i ∈ j0) j Hj).
An exact proof term for the current goal is (HWofTx j HjI).
We prove the intermediate claim HWgtSubW: ∀i : set, i ∈ I → Wgt i ⊆ W.
Let i be given.
Assume Hi: i ∈ I.
Let w be given.
Assume Hw: w ∈ Wgt i.
Apply (ReplE_impred (Igt i) (λj : set ⇒ Wof j) w Hw (w ∈ W)) to the current goal.
Let j be given.
Assume Hj: j ∈ Igt i.
Assume Heq: w = Wof j.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HjI: j ∈ I.
An exact proof term for the current goal is (SepE1 I (λj0 : set ⇒ i ∈ j0) j Hj).
An exact proof term for the current goal is (HWofW j HjI).
We prove the intermediate claim HLaterUTx: ∀i : set, i ∈ I → LaterU i ∈ Tx.
Let i be given.
Assume Hi: i ∈ I.
An exact proof term for the current goal is (topology_union_axiom X Tx HTx (Wgt i) (HWgtPowTx i Hi)).
We prove the intermediate claim HLaterUSubU: ∀i : set, i ∈ I → LaterU i ⊆ ⋃ W.
Let i be given.
Assume Hi: i ∈ I.
Let x be given.
Assume Hx: x ∈ LaterU i.
Apply (UnionE_impred (Wgt i) x Hx) to the current goal.
Let w be given.
Assume Hxw: x ∈ w.
Assume Hw: w ∈ Wgt i.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (HWgtSubW i Hi w Hw).
An exact proof term for the current goal is (UnionI W x w Hxw HwW).
We prove the intermediate claim Hshrink_step: ∀i A : set, i ∈ I → closed_in X Tx A → A ⊆ (Wof i) ∪ (LaterU i) → ∃U0 : set, U0 ∈ Tx ∧ (A ∖ (LaterU i)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof i) ∧ (A ∖ U0) ⊆ (LaterU i).
Let i and A be given.
Assume Hi: i ∈ I.
Assume HAcl: closed_in X Tx A.
Assume HAcov: A ⊆ (Wof i) ∪ (LaterU i).
We prove the intermediate claim HWofiTx: (Wof i) ∈ Tx.
An exact proof term for the current goal is (HWofTx i Hi).
We prove the intermediate claim HLTx: (LaterU i) ∈ Tx.
An exact proof term for the current goal is (HLaterUTx i Hi).
An exact proof term for the current goal is (normal_space_shrink_closed_cover2 X Tx A (Wof i) (LaterU i) Hnorm HAcl HWofiTx HLTx HAcov).
We prove the intermediate claim Hmax_cover_index: ∀x : set, x ∈ X → ∃imax : set, imax ∈ I ∧ x ∈ Wof imax ∧ ∀j : set, j ∈ I → imax ∈ j → x ∉ Wof j.
An exact proof term for the current goal is (point_finite_cover_has_max_index X W I idx Wof HordI HWcovers HWpointFin HidxI HpickW HpickW_idx).
Set PrevFam to be the term λi : set ⇒ λf : set → set ⇒ {f j|j ∈ i}.
Set RemA to be the term λi : set ⇒ λf : set → set ⇒ X ∖ ⋃ (PrevFam i f).
Set Cand to be the term λi : set ⇒ λf : set → set ⇒ {U0 ∈ Tx|((RemA i f) ∖ (LaterU i)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof i) ∧ ((RemA i f) ∖ U0) ⊆ (LaterU i)}.
Set StepU to be the term λi : set ⇒ λf : set → set ⇒ Eps_i (λU0 : set ⇒ U0 ∈ (Cand i f)).
We prove the intermediate claim HStepUext: ∀A : set, ∀g h : set → set, (∀x ∈ A, g x = h x) → StepU A g = StepU A h.
Let A, g and h be given.
Assume Hgh: ∀x ∈ A, g x = h x.
We prove the intermediate claim HPrevEq: PrevFam A g = PrevFam A h.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ PrevFam A g.
We will prove y ∈ PrevFam A h.
Apply (ReplE_impred A (λj0 : set ⇒ g j0) y Hy (y ∈ PrevFam A h)) to the current goal.
Let j be given.
Assume Hj: j ∈ A.
Assume Hey: y = g j.
We prove the intermediate claim Hgj: g j = h j.
An exact proof term for the current goal is (Hgh j Hj).
rewrite the current goal using Hey (from left to right).
rewrite the current goal using Hgj (from left to right).
An exact proof term for the current goal is (ReplI A (λj0 : set ⇒ h j0) j Hj).
Let y be given.
Assume Hy: y ∈ PrevFam A h.
We will prove y ∈ PrevFam A g.
Apply (ReplE_impred A (λj0 : set ⇒ h j0) y Hy (y ∈ PrevFam A g)) to the current goal.
Let j be given.
Assume Hj: j ∈ A.
Assume Hey: y = h j.
We prove the intermediate claim Hgj: g j = h j.
An exact proof term for the current goal is (Hgh j Hj).
rewrite the current goal using Hey (from left to right).
rewrite the current goal using Hgj (from right to left).
An exact proof term for the current goal is (ReplI A (λj0 : set ⇒ g j0) j Hj).
We prove the intermediate claim HRemEq: RemA A g = RemA A h.
We prove the intermediate claim HRemG: RemA A g = X ∖ ⋃ (PrevFam A g).
Use reflexivity.
We prove the intermediate claim HRemH: RemA A h = X ∖ ⋃ (PrevFam A h).
Use reflexivity.
rewrite the current goal using HRemG (from left to right).
rewrite the current goal using HRemH (from left to right).
We prove the intermediate claim HUnionEq: ⋃ (PrevFam A g) = ⋃ (PrevFam A h).
rewrite the current goal using HPrevEq (from left to right).
Use reflexivity.
rewrite the current goal using HUnionEq (from left to right).
Use reflexivity.
We prove the intermediate claim HCandEq: Cand A g = Cand A h.
Apply set_ext to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Cand A g.
We will prove U0 ∈ Cand A h.
We prove the intermediate claim HCg: Cand A g = {U ∈ Tx|((RemA A g) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A g) ∖ U) ⊆ (LaterU A)}.
Use reflexivity.
We prove the intermediate claim HCh: Cand A h = {U ∈ Tx|((RemA A h) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A h) ∖ U) ⊆ (LaterU A)}.
Use reflexivity.
We prove the intermediate claim HU0in: U0 ∈ {U ∈ Tx|((RemA A g) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A g) ∖ U) ⊆ (LaterU A)}.
rewrite the current goal using HCg (from right to left).
An exact proof term for the current goal is HU0.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU : set ⇒ ((RemA A g) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A g) ∖ U) ⊆ (LaterU A)) U0 HU0in).
We prove the intermediate claim HU0prop: ((RemA A g) ∖ (LaterU A)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof A) ∧ ((RemA A g) ∖ U0) ⊆ (LaterU A).
An exact proof term for the current goal is (SepE2 Tx (λU : set ⇒ ((RemA A g) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A g) ∖ U) ⊆ (LaterU A)) U0 HU0in).
We prove the intermediate claim HU0prop2: ((RemA A h) ∖ (LaterU A)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof A) ∧ ((RemA A h) ∖ U0) ⊆ (LaterU A).
rewrite the current goal using HRemEq (from right to left).
An exact proof term for the current goal is HU0prop.
An exact proof term for the current goal is (SepI Tx (λU : set ⇒ ((RemA A h) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A h) ∖ U) ⊆ (LaterU A)) U0 HU0Tx HU0prop2).
Let U0 be given.
Assume HU0: U0 ∈ Cand A h.
We will prove U0 ∈ Cand A g.
We prove the intermediate claim HCg: Cand A g = {U ∈ Tx|((RemA A g) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A g) ∖ U) ⊆ (LaterU A)}.
Use reflexivity.
We prove the intermediate claim HCh: Cand A h = {U ∈ Tx|((RemA A h) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A h) ∖ U) ⊆ (LaterU A)}.
Use reflexivity.
We prove the intermediate claim HU0in: U0 ∈ {U ∈ Tx|((RemA A h) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A h) ∖ U) ⊆ (LaterU A)}.
rewrite the current goal using HCh (from right to left).
An exact proof term for the current goal is HU0.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU : set ⇒ ((RemA A h) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A h) ∖ U) ⊆ (LaterU A)) U0 HU0in).
We prove the intermediate claim HU0prop: ((RemA A h) ∖ (LaterU A)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof A) ∧ ((RemA A h) ∖ U0) ⊆ (LaterU A).
An exact proof term for the current goal is (SepE2 Tx (λU : set ⇒ ((RemA A h) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A h) ∖ U) ⊆ (LaterU A)) U0 HU0in).
We prove the intermediate claim HU0prop2: ((RemA A g) ∖ (LaterU A)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof A) ∧ ((RemA A g) ∖ U0) ⊆ (LaterU A).
rewrite the current goal using HRemEq (from left to right).
An exact proof term for the current goal is HU0prop.
An exact proof term for the current goal is (SepI Tx (λU : set ⇒ ((RemA A g) ∖ (LaterU A)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof A) ∧ ((RemA A g) ∖ U) ⊆ (LaterU A)) U0 HU0Tx HU0prop2).
We prove the intermediate claim HStepG: StepU A g = Eps_i (λU0 : set ⇒ U0 ∈ Cand A g).
Use reflexivity.
We prove the intermediate claim HStepH: StepU A h = Eps_i (λU0 : set ⇒ U0 ∈ Cand A h).
Use reflexivity.
rewrite the current goal using HStepG (from left to right).
rewrite the current goal using HStepH (from left to right).
rewrite the current goal using HCandEq (from left to right).
Use reflexivity.
Set Ufun to be the term In_rec_i StepU.
We prove the intermediate claim HUfunEq: ∀i : set, Ufun i = StepU i Ufun.
Let i be given.
An exact proof term for the current goal is (In_rec_i_eq StepU HStepUext i).
We prove the intermediate claim HCandNonempty: ∀i : set, i ∈ I → ∃U0 : set, U0 ∈ Cand i Ufun.
Set p to be the term λalpha : set ⇒ alpha ∈ I → ∃U0 : set, U0 ∈ Cand alpha Ufun.
We prove the intermediate claim HpStep: ∀alpha : set, ordinal alpha → (∀beta ∈ alpha, p beta) → p alpha.
Let alpha be given.
Assume HordA: ordinal alpha.
Assume HIH: ∀beta ∈ alpha, p beta.
We will prove p alpha.
Assume HaI: alpha ∈ I.
We prove the intermediate claim HTransA: TransSet alpha.
An exact proof term for the current goal is (ordinal_TransSet alpha HordA).
We prove the intermediate claim HPrevPowTx: PrevFam alpha Ufun ∈ 𝒫 Tx.
Apply PowerI to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ PrevFam alpha Ufun.
Apply (ReplE_impred alpha (λj0 : set ⇒ Ufun j0) U0 HU0 (U0 ∈ Tx)) to the current goal.
Let j be given.
Assume Hj: j ∈ alpha.
Assume Heq: U0 = Ufun j.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HjI: j ∈ I.
We prove the intermediate claim HasubI: alpha ⊆ I.
An exact proof term for the current goal is (HTransI alpha HaI).
An exact proof term for the current goal is (HasubI j Hj).
We prove the intermediate claim Hpj: p j.
An exact proof term for the current goal is (HIH j Hj).
We prove the intermediate claim HexCandj: ∃Vj : set, Vj ∈ Cand j Ufun.
An exact proof term for the current goal is (Hpj HjI).
We prove the intermediate claim Hstepj: StepU j Ufun ∈ Cand j Ufun.
An exact proof term for the current goal is (Eps_i_ex (λVj : set ⇒ Vj ∈ Cand j Ufun) HexCandj).
We prove the intermediate claim HUfunjCand: Ufun j ∈ Cand j Ufun.
We prove the intermediate claim HUfunEqj: Ufun j = StepU j Ufun.
An exact proof term for the current goal is (HUfunEq j).
rewrite the current goal using HUfunEqj (from left to right) at position 1.
An exact proof term for the current goal is Hstepj.
An exact proof term for the current goal is (SepE1 Tx (λVj : set ⇒ ((RemA j Ufun) ∖ (LaterU j)) ⊆ Vj ∧ closure_of X Tx Vj ⊆ (Wof j) ∧ ((RemA j Ufun) ∖ Vj) ⊆ (LaterU j)) (Ufun j) HUfunjCand).
We prove the intermediate claim HUnionTx: ⋃ (PrevFam alpha Ufun) ∈ Tx.
An exact proof term for the current goal is (topology_union_axiom X Tx HTx (PrevFam alpha Ufun) HPrevPowTx).
We prove the intermediate claim HRemDef: RemA alpha Ufun = X ∖ ⋃ (PrevFam alpha Ufun).
Use reflexivity.
We prove the intermediate claim HRemClosed: closed_in X Tx (RemA alpha Ufun).
rewrite the current goal using HRemDef (from left to right).
An exact proof term for the current goal is (closed_of_open_complement X Tx (⋃ (PrevFam alpha Ufun)) HTx HUnionTx).
We prove the intermediate claim HRemCov: RemA alpha Ufun ⊆ (Wof alpha) ∪ (LaterU alpha).
Let x be given.
Assume HxA: x ∈ RemA alpha Ufun.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (⋃ (PrevFam alpha Ufun)) x HxA).
We prove the intermediate claim HxNotPrev: x ∉ ⋃ (PrevFam alpha Ufun).
An exact proof term for the current goal is (setminusE2 X (⋃ (PrevFam alpha Ufun)) x HxA).
We prove the intermediate claim Hexmax: ∃imax : set, imax ∈ I ∧ x ∈ Wof imax ∧ ∀j : set, j ∈ I → imax ∈ j → x ∉ Wof j.
An exact proof term for the current goal is (Hmax_cover_index x HxX).
Apply Hexmax to the current goal.
Let imax be given.
Assume HimaxPack: imax ∈ I ∧ x ∈ Wof imax ∧ ∀j : set, j ∈ I → imax ∈ j → x ∉ Wof j.
We prove the intermediate claim Himax12: imax ∈ I ∧ x ∈ Wof imax.
An exact proof term for the current goal is (andEL (imax ∈ I ∧ x ∈ Wof imax) (∀j : set, j ∈ I → imax ∈ j → x ∉ Wof j) HimaxPack).
We prove the intermediate claim HmaxProp: ∀j : set, j ∈ I → imax ∈ j → x ∉ Wof j.
An exact proof term for the current goal is (andER (imax ∈ I ∧ x ∈ Wof imax) (∀j : set, j ∈ I → imax ∈ j → x ∉ Wof j) HimaxPack).
We prove the intermediate claim HimaxI: imax ∈ I.
An exact proof term for the current goal is (andEL (imax ∈ I) (x ∈ Wof imax) Himax12).
We prove the intermediate claim HxWimax: x ∈ Wof imax.
An exact proof term for the current goal is (andER (imax ∈ I) (x ∈ Wof imax) Himax12).
We prove the intermediate claim HordMax: ordinal imax.
An exact proof term for the current goal is (ordinal_Hered I HordI imax HimaxI).
We prove the intermediate claim HordAlpha: ordinal alpha.
An exact proof term for the current goal is (ordinal_Hered I HordI alpha HaI).
Apply (ordinal_trichotomy_or_impred imax alpha HordMax HordAlpha (x ∈ (Wof alpha) ∪ (LaterU alpha))) to the current goal.
Assume HimaxLt: imax ∈ alpha.
Apply FalseE to the current goal.
We prove the intermediate claim Hpj: p imax.
An exact proof term for the current goal is (HIH imax HimaxLt).
We prove the intermediate claim HexCandImax: ∃V : set, V ∈ Cand imax Ufun.
An exact proof term for the current goal is (Hpj HimaxI).
We prove the intermediate claim Hstepimax: StepU imax Ufun ∈ Cand imax Ufun.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ V ∈ Cand imax Ufun) HexCandImax).
We prove the intermediate claim HUfunImaxCand: Ufun imax ∈ Cand imax Ufun.
We prove the intermediate claim HUfunEqimax: Ufun imax = StepU imax Ufun.
An exact proof term for the current goal is (HUfunEq imax).
rewrite the current goal using HUfunEqimax (from left to right) at position 1.
An exact proof term for the current goal is Hstepimax.
We prove the intermediate claim HUfunImaxProp: ((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax) ∧ closure_of X Tx (Ufun imax) ⊆ (Wof imax) ∧ ((RemA imax Ufun) ∖ (Ufun imax)) ⊆ (LaterU imax).
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ ((RemA imax Ufun) ∖ (LaterU imax)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof imax) ∧ ((RemA imax Ufun) ∖ U0) ⊆ (LaterU imax)) (Ufun imax) HUfunImaxCand).
We prove the intermediate claim HUfunImaxPQ: ((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax) ∧ closure_of X Tx (Ufun imax) ⊆ (Wof imax).
An exact proof term for the current goal is (andEL (((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax) ∧ closure_of X Tx (Ufun imax) ⊆ (Wof imax)) (((RemA imax Ufun) ∖ (Ufun imax)) ⊆ (LaterU imax)) HUfunImaxProp).
We prove the intermediate claim HUfunImaxSub: ((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax).
An exact proof term for the current goal is (andEL (((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax)) (closure_of X Tx (Ufun imax) ⊆ (Wof imax)) HUfunImaxPQ).
We prove the intermediate claim HPrevSub: PrevFam imax Ufun ⊆ PrevFam alpha Ufun.
Let y be given.
Assume Hy: y ∈ PrevFam imax Ufun.
Apply (ReplE_impred imax (λj0 : set ⇒ Ufun j0) y Hy (y ∈ PrevFam alpha Ufun)) to the current goal.
Let j be given.
Assume Hj: j ∈ imax.
Assume Hey: y = Ufun j.
We prove the intermediate claim HimaxSubAlpha: imax ⊆ alpha.
An exact proof term for the current goal is (HTransA imax HimaxLt).
We prove the intermediate claim HjA: j ∈ alpha.
An exact proof term for the current goal is (HimaxSubAlpha j Hj).
rewrite the current goal using Hey (from left to right).
An exact proof term for the current goal is (ReplI alpha (λj0 : set ⇒ Ufun j0) j HjA).
We prove the intermediate claim HUnionSub: ⋃ (PrevFam imax Ufun) ⊆ ⋃ (PrevFam alpha Ufun).
Let z be given.
Assume Hz: z ∈ ⋃ (PrevFam imax Ufun).
Apply (UnionE_impred (PrevFam imax Ufun) z Hz (z ∈ ⋃ (PrevFam alpha Ufun))) to the current goal.
Let y be given.
Assume Hzy: z ∈ y.
Assume Hy: y ∈ PrevFam imax Ufun.
We prove the intermediate claim HyA: y ∈ PrevFam alpha Ufun.
An exact proof term for the current goal is (HPrevSub y Hy).
An exact proof term for the current goal is (UnionI (PrevFam alpha Ufun) z y Hzy HyA).
We prove the intermediate claim HxNotPrevImax: x ∉ ⋃ (PrevFam imax Ufun).
Assume HxU: x ∈ ⋃ (PrevFam imax Ufun).
Apply HxNotPrev to the current goal.
An exact proof term for the current goal is (HUnionSub x HxU).
We prove the intermediate claim HxRemImax: x ∈ RemA imax Ufun.
An exact proof term for the current goal is (setminusI X (⋃ (PrevFam imax Ufun)) x HxX HxNotPrevImax).
We prove the intermediate claim HxNotLaterImax: x ∉ (LaterU imax).
Assume HxL: x ∈ LaterU imax.
Apply (UnionE_impred (Wgt imax) x HxL False) to the current goal.
Let w be given.
Assume Hxw: x ∈ w.
Assume Hw: w ∈ Wgt imax.
Apply (ReplE_impred (Igt imax) (λj0 : set ⇒ Wof j0) w Hw False) to the current goal.
Let j be given.
Assume Hj: j ∈ Igt imax.
Assume Heq: w = Wof j.
We prove the intermediate claim HjI: j ∈ I.
An exact proof term for the current goal is (SepE1 I (λj0 : set ⇒ imax ∈ j0) j Hj).
We prove the intermediate claim HimaxLj: imax ∈ j.
An exact proof term for the current goal is (SepE2 I (λj0 : set ⇒ imax ∈ j0) j Hj).
We prove the intermediate claim HxWj: x ∈ Wof j.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hxw.
An exact proof term for the current goal is ((HmaxProp j HjI HimaxLj) HxWj).
We prove the intermediate claim HxInDiff: x ∈ ((RemA imax Ufun) ∖ (LaterU imax)).
An exact proof term for the current goal is (setminusI (RemA imax Ufun) (LaterU imax) x HxRemImax HxNotLaterImax).
We prove the intermediate claim HxUimax: x ∈ Ufun imax.
An exact proof term for the current goal is (HUfunImaxSub x HxInDiff).
We prove the intermediate claim HUimaxPrev: Ufun imax ∈ PrevFam alpha Ufun.
An exact proof term for the current goal is (ReplI alpha (λj0 : set ⇒ Ufun j0) imax HimaxLt).
We prove the intermediate claim HxPrev: x ∈ ⋃ (PrevFam alpha Ufun).
An exact proof term for the current goal is (UnionI (PrevFam alpha Ufun) x (Ufun imax) HxUimax HUimaxPrev).
An exact proof term for the current goal is (HxNotPrev HxPrev).
Assume Heq: imax = alpha.
Apply binunionI1 to the current goal.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HxWimax.
Assume Hgt: alpha ∈ imax.
Apply binunionI2 to the current goal.
We prove the intermediate claim HimaxInIgt: imax ∈ Igt alpha.
An exact proof term for the current goal is (SepI I (λj0 : set ⇒ alpha ∈ j0) imax HimaxI Hgt).
We prove the intermediate claim HWi: Wof imax ∈ Wgt alpha.
An exact proof term for the current goal is (ReplI (Igt alpha) (λj0 : set ⇒ Wof j0) imax HimaxInIgt).
We prove the intermediate claim HxLater: x ∈ ⋃ (Wgt alpha).
An exact proof term for the current goal is (UnionI (Wgt alpha) x (Wof imax) HxWimax HWi).
An exact proof term for the current goal is HxLater.
We prove the intermediate claim HexStep: ∃U0 : set, U0 ∈ Tx ∧ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof alpha) ∧ ((RemA alpha Ufun) ∖ U0) ⊆ (LaterU alpha).
An exact proof term for the current goal is (Hshrink_step alpha (RemA alpha Ufun) HaI HRemClosed HRemCov).
Apply HexStep to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof alpha) ∧ ((RemA alpha Ufun) ∖ U0) ⊆ (LaterU alpha).
We use U0 to witness the existential quantifier.
We prove the intermediate claim HU0left: (U0 ∈ Tx ∧ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0) ∧ closure_of X Tx U0 ⊆ (Wof alpha).
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0) ∧ closure_of X Tx U0 ⊆ (Wof alpha)) (((RemA alpha Ufun) ∖ U0) ⊆ (LaterU alpha)) HU0).
We prove the intermediate claim HU0R: ((RemA alpha Ufun) ∖ U0) ⊆ (LaterU alpha).
An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0) ∧ closure_of X Tx U0 ⊆ (Wof alpha)) (((RemA alpha Ufun) ∖ U0) ⊆ (LaterU alpha)) HU0).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0) (andEL (U0 ∈ Tx ∧ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0) (closure_of X Tx U0 ⊆ (Wof alpha)) HU0left)).
We prove the intermediate claim HU0P: ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0) (andEL (U0 ∈ Tx ∧ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0) (closure_of X Tx U0 ⊆ (Wof alpha)) HU0left)).
We prove the intermediate claim HU0Q: closure_of X Tx U0 ⊆ (Wof alpha).
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0) (closure_of X Tx U0 ⊆ (Wof alpha)) HU0left).
We prove the intermediate claim HU0propCand: ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U0 ∧ closure_of X Tx U0 ⊆ (Wof alpha) ∧ ((RemA alpha Ufun) ∖ U0) ⊆ (LaterU alpha).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU0P.
An exact proof term for the current goal is HU0Q.
An exact proof term for the current goal is HU0R.
An exact proof term for the current goal is (SepI Tx (λU : set ⇒ ((RemA alpha Ufun) ∖ (LaterU alpha)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof alpha) ∧ ((RemA alpha Ufun) ∖ U) ⊆ (LaterU alpha)) U0 HU0Tx HU0propCand).
We prove the intermediate claim HpAll: ∀a : set, ordinal a → p a.
An exact proof term for the current goal is (ordinal_ind p HpStep).
Let i be given.
Assume Hi: i ∈ I.
An exact proof term for the current goal is ((HpAll i (ordinal_Hered I HordI i Hi)) Hi).
We prove the intermediate claim HUfunCand: ∀i : set, i ∈ I → Ufun i ∈ Cand i Ufun.
Let i be given.
Assume Hi: i ∈ I.
We prove the intermediate claim Hex: ∃U0 : set, U0 ∈ Cand i Ufun.
An exact proof term for the current goal is (HCandNonempty i Hi).
We prove the intermediate claim Hstep: StepU i Ufun ∈ Cand i Ufun.
An exact proof term for the current goal is (Eps_i_ex (λU0 : set ⇒ U0 ∈ Cand i Ufun) Hex).
Set Ui to be the term Ufun i.
We prove the intermediate claim HUiDef: Ui = Ufun i.
Use reflexivity.
We prove the intermediate claim HUiEq: Ui = StepU i Ufun.
rewrite the current goal using HUiDef (from left to right).
An exact proof term for the current goal is (HUfunEq i).
We will prove Ufun i ∈ Cand i Ufun.
rewrite the current goal using HUiDef (from right to left).
rewrite the current goal using HUiEq (from left to right).
An exact proof term for the current goal is Hstep.
Set V to be the term {Ufun i|i ∈ I}.
We prove the intermediate claim HVopen: ∀v : set, v ∈ V → v ∈ Tx.
Let v be given.
Assume Hv: v ∈ V.
Apply (ReplE_impred I (λi0 : set ⇒ Ufun i0) v Hv (v ∈ Tx)) to the current goal.
Let i be given.
Assume Hi: i ∈ I.
Assume Heq: v = Ufun i.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HUiCand: Ufun i ∈ Cand i Ufun.
An exact proof term for the current goal is (HUfunCand i Hi).
An exact proof term for the current goal is (SepE1 Tx (λU : set ⇒ ((RemA i Ufun) ∖ (LaterU i)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof i) ∧ ((RemA i Ufun) ∖ U) ⊆ (LaterU i)) (Ufun i) HUiCand).
We prove the intermediate claim HVcover: covers X V.
Let x be given.
Assume HxX: x ∈ X.
Apply (Hmax_cover_index x HxX) to the current goal.
Let imax be given.
Assume Himax: imax ∈ I ∧ x ∈ Wof imax ∧ ∀j : set, j ∈ I → imax ∈ j → x ∉ Wof j.
We prove the intermediate claim HimaxI: imax ∈ I.
Apply Himax to the current goal.
Assume Hpair Hfor.
Apply Hpair to the current goal.
Assume Hi _Hx.
An exact proof term for the current goal is Hi.
We prove the intermediate claim Hforall: ∀j : set, j ∈ I → imax ∈ j → x ∉ Wof j.
Apply Himax to the current goal.
Assume _Hpair Hfor.
An exact proof term for the current goal is Hfor.
We prove the intermediate claim HnotLater: x ∉ LaterU imax.
Assume HxL: x ∈ LaterU imax.
Apply (UnionE_impred (Wgt imax) x HxL (False)) to the current goal.
Let w be given.
Assume Hxw: x ∈ w.
Assume Hw: w ∈ Wgt imax.
Apply (ReplE_impred (Igt imax) (λj0 : set ⇒ Wof j0) w Hw (False)) to the current goal.
Let j be given.
Assume Hjgt: j ∈ Igt imax.
Assume Heq: w = Wof j.
We prove the intermediate claim HjI: j ∈ I.
An exact proof term for the current goal is (SepE1 I (λj0 : set ⇒ imax ∈ j0) j Hjgt).
We prove the intermediate claim Himaxj: imax ∈ j.
An exact proof term for the current goal is (SepE2 I (λj0 : set ⇒ imax ∈ j0) j Hjgt).
We prove the intermediate claim HxWj: x ∈ Wof j.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hxw.
An exact proof term for the current goal is (Hforall j HjI Himaxj HxWj).
Apply (xm (x ∈ ⋃ (PrevFam imax Ufun))) to the current goal.
Assume HxPrev: x ∈ ⋃ (PrevFam imax Ufun).
Apply (UnionE_impred (PrevFam imax Ufun) x HxPrev (∃v : set, v ∈ V ∧ x ∈ v)) to the current goal.
Let v0 be given.
Assume Hxv0: x ∈ v0.
Assume Hv0: v0 ∈ PrevFam imax Ufun.
Apply (ReplE_impred imax (λj0 : set ⇒ Ufun j0) v0 Hv0 (∃v : set, v ∈ V ∧ x ∈ v)) to the current goal.
Let j be given.
Assume Hj: j ∈ imax.
Assume Hv0eq: v0 = Ufun j.
We prove the intermediate claim HimaxSubI: imax ⊆ I.
An exact proof term for the current goal is (HTransI imax HimaxI).
We prove the intermediate claim HjI: j ∈ I.
An exact proof term for the current goal is (HimaxSubI j Hj).
We use (Ufun j) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI I (λi0 : set ⇒ Ufun i0) j HjI).
rewrite the current goal using Hv0eq (from right to left).
An exact proof term for the current goal is Hxv0.
Assume HxNotPrev: x ∉ ⋃ (PrevFam imax Ufun).
We prove the intermediate claim HxRem: x ∈ RemA imax Ufun.
We prove the intermediate claim HRemDef: RemA imax Ufun = X ∖ ⋃ (PrevFam imax Ufun).
Use reflexivity.
rewrite the current goal using HRemDef (from left to right).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxNotPrev.
We prove the intermediate claim HUiCand: Ufun imax ∈ Cand imax Ufun.
An exact proof term for the current goal is (HUfunCand imax HimaxI).
We prove the intermediate claim HUiProp: ((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax) ∧ closure_of X Tx (Ufun imax) ⊆ (Wof imax) ∧ ((RemA imax Ufun) ∖ (Ufun imax)) ⊆ (LaterU imax).
An exact proof term for the current goal is (SepE2 Tx (λU : set ⇒ ((RemA imax Ufun) ∖ (LaterU imax)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof imax) ∧ ((RemA imax Ufun) ∖ U) ⊆ (LaterU imax)) (Ufun imax) HUiCand).
We prove the intermediate claim Hsub: ((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax).
We prove the intermediate claim H12: (((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax)) ∧ (closure_of X Tx (Ufun imax) ⊆ (Wof imax)).
An exact proof term for the current goal is (andEL ((((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax)) ∧ (closure_of X Tx (Ufun imax) ⊆ (Wof imax))) (((RemA imax Ufun) ∖ (Ufun imax)) ⊆ (LaterU imax)) HUiProp).
An exact proof term for the current goal is (andEL (((RemA imax Ufun) ∖ (LaterU imax)) ⊆ (Ufun imax)) (closure_of X Tx (Ufun imax) ⊆ (Wof imax)) H12).
We prove the intermediate claim HxIn: x ∈ (RemA imax Ufun) ∖ (LaterU imax).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxRem.
An exact proof term for the current goal is HnotLater.
We use (Ufun imax) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI I (λi0 : set ⇒ Ufun i0) imax HimaxI).
An exact proof term for the current goal is (Hsub x HxIn).
We prove the intermediate claim HVcov: open_cover X Tx V.
We will prove (∀v : set, v ∈ V → v ∈ Tx) ∧ covers X V.
Apply andI to the current goal.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is HVcover.
We prove the intermediate claim HVclsubWof: ∀i : set, i ∈ I → closure_of X Tx (Ufun i) ⊆ (Wof i).
Let i be given.
Assume Hi: i ∈ I.
We prove the intermediate claim HUiCand: Ufun i ∈ Cand i Ufun.
An exact proof term for the current goal is (HUfunCand i Hi).
We prove the intermediate claim HUiProp: ((RemA i Ufun) ∖ (LaterU i)) ⊆ (Ufun i) ∧ closure_of X Tx (Ufun i) ⊆ (Wof i) ∧ ((RemA i Ufun) ∖ (Ufun i)) ⊆ (LaterU i).
An exact proof term for the current goal is (SepE2 Tx (λU : set ⇒ ((RemA i Ufun) ∖ (LaterU i)) ⊆ U ∧ closure_of X Tx U ⊆ (Wof i) ∧ ((RemA i Ufun) ∖ U) ⊆ (LaterU i)) (Ufun i) HUiCand).
We prove the intermediate claim H12: (((RemA i Ufun) ∖ (LaterU i)) ⊆ (Ufun i)) ∧ (closure_of X Tx (Ufun i) ⊆ (Wof i)).
An exact proof term for the current goal is (andEL ((((RemA i Ufun) ∖ (LaterU i)) ⊆ (Ufun i)) ∧ (closure_of X Tx (Ufun i) ⊆ (Wof i))) (((RemA i Ufun) ∖ (Ufun i)) ⊆ (LaterU i)) HUiProp).
An exact proof term for the current goal is (andER (((RemA i Ufun) ∖ (LaterU i)) ⊆ (Ufun i)) (closure_of X Tx (Ufun i) ⊆ (Wof i)) H12).
We prove the intermediate claim HVsubW: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w.
Let v be given.
Assume Hv: v ∈ V.
Apply (ReplE_impred I (λi0 : set ⇒ Ufun i0) v Hv (∃w : set, w ∈ W ∧ v ⊆ w)) to the current goal.
Let i be given.
Assume Hi: i ∈ I.
Assume Heq: v = Ufun i.
We use (Wof i) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HWofW i Hi).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hclsub: closure_of X Tx (Ufun i) ⊆ (Wof i).
An exact proof term for the current goal is (HVclsubWof i Hi).
We prove the intermediate claim HUiSubX: Ufun i ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx (Ufun i) HTx (HVopen (Ufun i) (ReplI I (λi0 : set ⇒ Ufun i0) i Hi))).
An exact proof term for the current goal is (Subq_tra (Ufun i) (closure_of X Tx (Ufun i)) (Wof i) (closure_contains_set X Tx (Ufun i) HTx HUiSubX) Hclsub).
We prove the intermediate claim HVclsubW: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
Let v be given.
Assume Hv: v ∈ V.
Apply (ReplE_impred I (λi0 : set ⇒ Ufun i0) v Hv (∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w)) to the current goal.
Let i be given.
Assume Hi: i ∈ I.
Assume Heq: v = Ufun i.
We use (Wof i) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HWofW i Hi).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (HVclsubWof i Hi).
We prove the intermediate claim HVlf: locally_finite_family X Tx V.
Set g to be the term λw : set ⇒ Ufun (idx w).
We prove the intermediate claim Hgsub: ∀w : set, w ∈ W → g w ⊆ w.
Let w be given.
Assume HwW: w ∈ W.
We prove the intermediate claim Hi: idx w ∈ I.
An exact proof term for the current goal is (HidxI w HwW).
We prove the intermediate claim Hclsub: closure_of X Tx (Ufun (idx w)) ⊆ (Wof (idx w)).
An exact proof term for the current goal is (HVclsubWof (idx w) Hi).
We prove the intermediate claim HWofi: Wof (idx w) = w.
We prove the intermediate claim HWdef: Wof (idx w) = pickW (idx w).
Use reflexivity.
rewrite the current goal using HWdef (from left to right).
An exact proof term for the current goal is (HpickW_idx w HwW).
We prove the intermediate claim Hclsubw: closure_of X Tx (Ufun (idx w)) ⊆ w.
rewrite the current goal using HWofi (from right to left) at position 2.
An exact proof term for the current goal is Hclsub.
We prove the intermediate claim HUsX: Ufun (idx w) ⊆ X.
Let z be given.
Assume Hz: z ∈ Ufun (idx w).
We prove the intermediate claim Hcl: z ∈ closure_of X Tx (Ufun (idx w)).
An exact proof term for the current goal is (closure_contains_set X Tx (Ufun (idx w)) HTx (topology_elem_subset X Tx (Ufun (idx w)) HTx (HVopen (Ufun (idx w)) (ReplI I (λi0 : set ⇒ Ufun i0) (idx w) Hi))) z Hz).
An exact proof term for the current goal is (HWsubX w HwW z (Hclsubw z Hcl)).
An exact proof term for the current goal is (Subq_tra (Ufun (idx w)) (closure_of X Tx (Ufun (idx w))) w (closure_contains_set X Tx (Ufun (idx w)) HTx HUsX) Hclsubw).
We prove the intermediate claim HVeq: V = {g w|w ∈ W}.
Apply set_ext to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Apply (ReplE_impred I (λi0 : set ⇒ Ufun i0) v HvV (v ∈ {g w|w ∈ W})) to the current goal.
Let i be given.
Assume Hi: i ∈ I.
Assume Heq: v = Ufun i.
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ idx w = i.
An exact proof term for the current goal is (HidxSurj i Hi).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ idx w = i.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (idx w = i) Hw).
We prove the intermediate claim Hidxw: idx w = i.
An exact proof term for the current goal is (andER (w ∈ W) (idx w = i) Hw).
rewrite the current goal using Heq (from left to right).
rewrite the current goal using Hidxw (from right to left).
An exact proof term for the current goal is (ReplI W (λw0 : set ⇒ g w0) w HwW).
Let v be given.
Assume Hv: v ∈ {g w|w ∈ W}.
Apply (ReplE_impred W (λw0 : set ⇒ g w0) v Hv (v ∈ V)) to the current goal.
Let w be given.
Assume HwW: w ∈ W.
Assume Heq: v = g w.
We prove the intermediate claim Hi: idx w ∈ I.
An exact proof term for the current goal is (HidxI w HwW).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (ReplI I (λi0 : set ⇒ Ufun i0) (idx w) Hi).
rewrite the current goal using HVeq (from left to right).
An exact proof term for the current goal is (locally_finite_family_Repl_subsets X Tx W g HWlf Hgsub).
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HVcov.
An exact proof term for the current goal is HVlf.
An exact proof term for the current goal is HVsubW.
An exact proof term for the current goal is HVclsubW.
∎