Let X, Tx and V be given.
Assume Hreg: regular_space X Tx.
Assume HVcov: open_cover X Tx V.
Assume Hsigma: sigma_locally_finite_family X Tx V.
We will prove ∃C : set, covers X C ∧ locally_finite_family X Tx C ∧ refine_of C V.
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 HVop: ∀v : set, v ∈ V → v ∈ Tx.
Let v be given.
Assume HvV: v ∈ V.
An exact proof term for the current goal is (open_cover_members_open X Tx V v HVcov HvV).
We prove the intermediate claim HVcovers: covers X V.
An exact proof term for the current goal is (open_cover_implies_covers X Tx V HVcov).
We prove the intermediate claim HexFams: ∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G) ∧ V = ⋃ Fams.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G) ∧ V = ⋃ Fams) Hsigma).
Apply HexFams to the current goal.
Let Fams be given.
Assume HFams: countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G) ∧ V = ⋃ Fams.
We prove the intermediate claim HFams_left: (countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X)) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G).
An exact proof term for the current goal is (andEL ((countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X)) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G)) (V = ⋃ Fams) HFams).
We prove the intermediate claim HAB: countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X).
An exact proof term for the current goal is (andEL (countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X)) (∀G : set, G ∈ Fams → locally_finite_family X Tx G) HFams_left).
We prove the intermediate claim HcountF: countable_set Fams.
An exact proof term for the current goal is (andEL (countable_set Fams) (Fams ⊆ 𝒫 (𝒫 X)) HAB).
We prove the intermediate claim HLFfam: ∀G : set, G ∈ Fams → locally_finite_family X Tx G.
An exact proof term for the current goal is (andER (countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X)) (∀G : set, G ∈ Fams → locally_finite_family X Tx G) HFams_left).
We prove the intermediate claim HVequiv: V = ⋃ Fams.
An exact proof term for the current goal is (andER ((countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X)) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G)) (V = ⋃ Fams) HFams).
We prove the intermediate claim HexEnc: ∃enc : set → set, inj Fams ω enc.
An exact proof term for the current goal is HcountF.
Apply HexEnc to the current goal.
Let enc be given.
Assume Henc: inj Fams ω enc.
Set HasIndex to be the term λn : set ⇒ ∃G : set, G ∈ Fams ∧ enc G = n.
Set B to be the term λn : set ⇒ if HasIndex n then inv Fams enc n else Empty.
Set Vset to be the term λn : set ⇒ ⋃ (B n).
Set Prev to be the term λn : set ⇒ ⋃i ∈ nVset i.
Set Cn to be the term λn : set ⇒ {U ∖ Prev n|U ∈ (B n)}.
Set CFams to be the term {Cn n|n ∈ ω}.
Set C to be the term ⋃ CFams.
We prove the intermediate claim HBsubV: ∀n : set, n ∈ ω → (B n) ⊆ V.
Let n be given.
Assume HnO: n ∈ ω.
Apply (xm (HasIndex n)) to the current goal.
Assume Hhas: HasIndex n.
We prove the intermediate claim HBdef: B n = inv Fams enc n.
An exact proof term for the current goal is (If_i_1 (HasIndex n) (inv Fams enc n) Empty Hhas).
rewrite the current goal using HBdef (from left to right).
Let u be given.
Assume Hu: u ∈ inv Fams enc n.
We will prove u ∈ V.
We prove the intermediate claim HexG: ∃G : set, G ∈ Fams ∧ enc G = n.
An exact proof term for the current goal is Hhas.
Apply HexG to the current goal.
Let G be given.
Assume HG: G ∈ Fams ∧ enc G = n.
We prove the intermediate claim HGin: G ∈ Fams.
An exact proof term for the current goal is (andEL (G ∈ Fams) (enc G = n) HG).
We prove the intermediate claim HGeq: enc G = n.
An exact proof term for the current goal is (andER (G ∈ Fams) (enc G = n) HG).
We prove the intermediate claim HinvEq: inv Fams enc n = G.
rewrite the current goal using HGeq (from right to left).
An exact proof term for the current goal is (inj_linv Fams enc (andER (∀u ∈ Fams, enc u ∈ ω) (∀u v ∈ Fams, enc u = enc v → u = v) Henc) G HGin).
We prove the intermediate claim HuG: u ∈ G.
rewrite the current goal using HinvEq (from right to left).
An exact proof term for the current goal is Hu.
rewrite the current goal using HVequiv (from left to right).
An exact proof term for the current goal is (UnionI Fams u G HuG HGin).
Assume Hno: ¬ HasIndex n.
We prove the intermediate claim HBdef: B n = Empty.
An exact proof term for the current goal is (If_i_0 (HasIndex n) (inv Fams enc n) Empty Hno).
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is (Subq_Empty V).
We prove the intermediate claim HB_lf: ∀n : set, n ∈ ω → locally_finite_family X Tx (B n).
Let n be given.
Assume HnO: n ∈ ω.
Apply (xm (HasIndex n)) to the current goal.
Assume Hhas: HasIndex n.
We prove the intermediate claim HBdef: B n = inv Fams enc n.
An exact proof term for the current goal is (If_i_1 (HasIndex n) (inv Fams enc n) Empty Hhas).
rewrite the current goal using HBdef (from left to right).
We prove the intermediate claim HexG: ∃G : set, G ∈ Fams ∧ enc G = n.
An exact proof term for the current goal is Hhas.
Apply HexG to the current goal.
Let G be given.
Assume HG: G ∈ Fams ∧ enc G = n.
We prove the intermediate claim HGin: G ∈ Fams.
An exact proof term for the current goal is (andEL (G ∈ Fams) (enc G = n) HG).
We prove the intermediate claim HGeq: enc G = n.
An exact proof term for the current goal is (andER (G ∈ Fams) (enc G = n) HG).
We prove the intermediate claim HinvEq: inv Fams enc n = G.
rewrite the current goal using HGeq (from right to left).
An exact proof term for the current goal is (inj_linv Fams enc (andER (∀u ∈ Fams, enc u ∈ ω) (∀u v ∈ Fams, enc u = enc v → u = v) Henc) G HGin).
rewrite the current goal using HinvEq (from left to right).
An exact proof term for the current goal is (HLFfam G HGin).
Assume Hno: ¬ HasIndex n.
We prove the intermediate claim HBdef: B n = Empty.
An exact proof term for the current goal is (If_i_0 (HasIndex n) (inv Fams enc n) Empty Hno).
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is (locally_finite_family_empty X Tx HTx).
We prove the intermediate claim HBinTx: ∀n : set, n ∈ ω → ∀U : set, U ∈ (B n) → U ∈ Tx.
Let n be given.
Assume HnO: n ∈ ω.
Let U be given.
Assume HU: U ∈ (B n).
We prove the intermediate claim HUinV: U ∈ V.
An exact proof term for the current goal is (HBsubV n HnO U HU).
An exact proof term for the current goal is (HVop U HUinV).
We prove the intermediate claim HrefCV: refine_of C V.
Let c be given.
Assume HcC: c ∈ C.
We will prove ∃u : set, u ∈ V ∧ c ⊆ u.
Apply (UnionE_impred CFams c HcC (∃u : set, u ∈ V ∧ c ⊆ u)) to the current goal.
Let C0 be given.
Assume HcC0: c ∈ C0.
Assume HC0: C0 ∈ CFams.
Apply (ReplE_impred ω (λn0 : set ⇒ Cn n0) C0 HC0 (∃u : set, u ∈ V ∧ c ⊆ u)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HC0eq: C0 = Cn n.
We prove the intermediate claim HcCn: c ∈ Cn n.
rewrite the current goal using HC0eq (from right to left).
An exact proof term for the current goal is HcC0.
Apply (ReplE_impred (B n) (λU0 : set ⇒ U0 ∖ Prev n) c HcCn (∃u : set, u ∈ V ∧ c ⊆ u)) to the current goal.
Let U be given.
Assume HU: U ∈ (B n).
Assume Hceq: c = U ∖ Prev n.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HBsubV n HnO U HU).
rewrite the current goal using Hceq (from left to right).
An exact proof term for the current goal is (setminus_Subq U (Prev n)).
We prove the intermediate claim HcovC: covers X C.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hexv: ∃v : set, v ∈ V ∧ x ∈ v.
An exact proof term for the current goal is (HVcovers x HxX).
Apply Hexv to the current goal.
Let v be given.
Assume Hv: v ∈ V ∧ x ∈ v.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (andEL (v ∈ V) (x ∈ v) Hv).
We prove the intermediate claim Hxv: x ∈ v.
An exact proof term for the current goal is (andER (v ∈ V) (x ∈ v) Hv).
We prove the intermediate claim HvUF: v ∈ ⋃ Fams.
rewrite the current goal using HVequiv (from right to left).
An exact proof term for the current goal is HvV.
Apply (UnionE_impred Fams v HvUF (∃u : set, u ∈ C ∧ x ∈ u)) to the current goal.
Let G be given.
Assume HvG: v ∈ G.
Assume HGin: G ∈ Fams.
We prove the intermediate claim HnO: enc G ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Fams, enc u ∈ ω) (∀u v ∈ Fams, enc u = enc v → u = v) Henc G HGin).
Set Pn to be the term λn0 : set ⇒ n0 ∈ ω ∧ ∃U : set, U ∈ (B n0) ∧ x ∈ U.
We prove the intermediate claim HexPn: ∃n0 : set, ordinal n0 ∧ Pn n0.
We use (enc G) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_ordinal (enc G) (omega_nat_p (enc G) HnO)).
We will prove (enc G ∈ ω ∧ ∃U : set, U ∈ (B (enc G)) ∧ x ∈ U).
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
We prove the intermediate claim Hhas: HasIndex (enc G).
We will prove ∃G0 : set, G0 ∈ Fams ∧ enc G0 = enc G.
We use G to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HGin.
Use reflexivity.
We prove the intermediate claim HBdef: B (enc G) = inv Fams enc (enc G).
An exact proof term for the current goal is (If_i_1 (HasIndex (enc G)) (inv Fams enc (enc G)) Empty Hhas).
We prove the intermediate claim HinvEq: inv Fams enc (enc G) = G.
An exact proof term for the current goal is (inj_linv Fams enc (andER (∀u ∈ Fams, enc u ∈ ω) (∀u v ∈ Fams, enc u = enc v → u = v) Henc) G HGin).
We use v to witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using HBdef (from left to right).
rewrite the current goal using HinvEq (from left to right).
An exact proof term for the current goal is HvG.
An exact proof term for the current goal is Hxv.
Apply (least_ordinal_ex Pn HexPn) to the current goal.
Let N be given.
Assume HNpack: ordinal N ∧ Pn N ∧ ∀m ∈ N, ¬ Pn m.
We prove the intermediate claim HNP: Pn N.
An exact proof term for the current goal is (andER (ordinal N) (Pn N) (andEL (ordinal N ∧ Pn N) (∀m ∈ N, ¬ Pn m) HNpack)).
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (∃U : set, U ∈ (B N) ∧ x ∈ U) HNP).
We prove the intermediate claim HexUN: ∃U : set, U ∈ (B N) ∧ x ∈ U.
An exact proof term for the current goal is (andER (N ∈ ω) (∃U : set, U ∈ (B N) ∧ x ∈ U) HNP).
Apply HexUN to the current goal.
Let U be given.
Assume HUN: U ∈ (B N) ∧ x ∈ U.
We prove the intermediate claim HUNin: U ∈ (B N).
An exact proof term for the current goal is (andEL (U ∈ (B N)) (x ∈ U) HUN).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ (B N)) (x ∈ U) HUN).
We prove the intermediate claim HxNotPrev: x ∉ Prev N.
Assume HxPrev: x ∈ Prev N.
Apply (famunionE_impred N (λi : set ⇒ Vset i) x HxPrev False) to the current goal.
Let i be given.
Assume HiN: i ∈ N.
Assume Hxi: x ∈ Vset i.
We prove the intermediate claim HexUi: ∃Ui : set, Ui ∈ (B i) ∧ x ∈ Ui.
Apply (UnionE_impred (B i) x Hxi (∃Ui : set, Ui ∈ (B i) ∧ x ∈ Ui)) to the current goal.
Let Ui be given.
Assume HxUi: x ∈ Ui.
Assume HUi: Ui ∈ (B i).
We use Ui to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUi.
An exact proof term for the current goal is HxUi.
We prove the intermediate claim HPni: Pn i.
We will prove (i ∈ ω ∧ ∃U : set, U ∈ (B i) ∧ x ∈ U).
Apply andI to the current goal.
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (omega_TransSet N HNO i HiN).
An exact proof term for the current goal is HiO.
An exact proof term for the current goal is HexUi.
We prove the intermediate claim Hmin: ∀m ∈ N, ¬ Pn m.
An exact proof term for the current goal is (andER (ordinal N ∧ Pn N) (∀m ∈ N, ¬ Pn m) HNpack).
An exact proof term for the current goal is ((Hmin i HiN) HPni).
We use (U ∖ Prev N) to witness the existential quantifier.
Apply andI to the current goal.
We will prove (U ∖ Prev N) ∈ C.
We prove the intermediate claim HCnin: Cn N ∈ CFams.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ Cn n0) N HNO).
We prove the intermediate claim HUinCn: U ∖ Prev N ∈ Cn N.
An exact proof term for the current goal is (ReplI (B N) (λU0 : set ⇒ U0 ∖ Prev N) U HUNin).
An exact proof term for the current goal is (UnionI CFams (U ∖ Prev N) (Cn N) HUinCn HCnin).
We will prove x ∈ U ∖ Prev N.
An exact proof term for the current goal is (setminusI U (Prev N) x HxU HxNotPrev).
We prove the intermediate claim HLF_C: locally_finite_family X Tx C.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N0 : set, N0 ∈ Tx ∧ x ∈ N0 ∧ ∃S0 : set, finite S0 ∧ S0 ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N0 ≠ Empty → A ∈ 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 Hexv: ∃v : set, v ∈ V ∧ x ∈ v.
An exact proof term for the current goal is (HVcovers x HxX).
Apply Hexv to the current goal.
Let v be given.
Assume Hv: v ∈ V ∧ x ∈ v.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (andEL (v ∈ V) (x ∈ v) Hv).
We prove the intermediate claim Hxv: x ∈ v.
An exact proof term for the current goal is (andER (v ∈ V) (x ∈ v) Hv).
We prove the intermediate claim HvTx: v ∈ Tx.
An exact proof term for the current goal is (HVop v HvV).
We prove the intermediate claim HvUF: v ∈ ⋃ Fams.
rewrite the current goal using HVequiv (from right to left).
An exact proof term for the current goal is HvV.
Apply (UnionE_impred Fams v HvUF (∃N0 : set, N0 ∈ Tx ∧ x ∈ N0 ∧ ∃S0 : set, finite S0 ∧ S0 ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N0 ≠ Empty → A ∈ S0)) to the current goal.
Let G be given.
Assume HvG: v ∈ G.
Assume HGin: G ∈ Fams.
We prove the intermediate claim HNO: enc G ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Fams, enc u ∈ ω) (∀u v ∈ Fams, enc u = enc v → u = v) Henc G HGin).
Set N to be the term enc G.
We prove the intermediate claim HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNO).
Set I to be the term ordsucc N.
We prove the intermediate claim HIomega: ∀i : set, i ∈ I → i ∈ ω.
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim HIinO: I ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNO).
We prove the intermediate claim HIsubO: I ⊆ ω.
An exact proof term for the current goal is (omega_TransSet I HIinO).
An exact proof term for the current goal is (HIsubO i HiI).
We prove the intermediate claim HI_fin: finite I.
An exact proof term for the current goal is (nat_finite I (nat_ordsucc N HNnat)).
We prove the intermediate claim Hhas: HasIndex N.
We will prove ∃G0 : set, G0 ∈ Fams ∧ enc G0 = N.
We use G to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HGin.
Use reflexivity.
We prove the intermediate claim HBdefN: B N = inv Fams enc N.
An exact proof term for the current goal is (If_i_1 (HasIndex N) (inv Fams enc N) Empty Hhas).
We prove the intermediate claim HinvEqN: inv Fams enc N = G.
An exact proof term for the current goal is (inj_linv Fams enc (andER (∀u ∈ Fams, enc u ∈ ω) (∀u v ∈ Fams, enc u = enc v → u = v) Henc) G HGin).
We prove the intermediate claim HvBN: v ∈ (B N).
rewrite the current goal using HBdefN (from left to right).
rewrite the current goal using HinvEqN (from left to right).
An exact proof term for the current goal is HvG.
Set GoodNbhd to be the term λi : set ⇒ λN1 : set ⇒ N1 ∈ Tx ∧ x ∈ N1 ∧ ∃S1 : set, finite S1 ∧ S1 ⊆ (B i) ∧ ∀A : set, A ∈ (B i) → A ∩ N1 ≠ Empty → A ∈ S1.
Set Nbhd to be the term λi : set ⇒ Eps_i (GoodNbhd i).
We prove the intermediate claim HNbhd: ∀i : set, i ∈ I → GoodNbhd i (Nbhd i).
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (HIomega i HiI).
We prove the intermediate claim HlfBi: locally_finite_family X Tx (B i).
An exact proof term for the current goal is (HB_lf i HiO).
We prove the intermediate claim HexN1: ∃N1 : set, GoodNbhd i N1.
An exact proof term for the current goal is (locally_finite_family_property X Tx (B i) HlfBi x HxX).
Apply HexN1 to the current goal.
Let N1 be given.
Assume HN1: GoodNbhd i N1.
An exact proof term for the current goal is (Eps_i_ax (GoodNbhd i) N1 HN1).
We prove the intermediate claim HNbhdTx: ∀i : set, i ∈ I → (Nbhd i) ∈ Tx.
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim Hprop: GoodNbhd i (Nbhd i).
An exact proof term for the current goal is (HNbhd i HiI).
We prove the intermediate claim Hleft: (Nbhd i ∈ Tx ∧ x ∈ Nbhd i).
An exact proof term for the current goal is (andEL (Nbhd i ∈ Tx ∧ x ∈ Nbhd i) (∃S1 : set, finite S1 ∧ S1 ⊆ (B i) ∧ ∀A : set, A ∈ (B i) → A ∩ Nbhd i ≠ Empty → A ∈ S1) Hprop).
An exact proof term for the current goal is (andEL (Nbhd i ∈ Tx) (x ∈ Nbhd i) Hleft).
We prove the intermediate claim HNbhdx: ∀i : set, i ∈ I → x ∈ Nbhd i.
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim Hprop: GoodNbhd i (Nbhd i).
An exact proof term for the current goal is (HNbhd i HiI).
We prove the intermediate claim Hleft: (Nbhd i ∈ Tx ∧ x ∈ Nbhd i).
An exact proof term for the current goal is (andEL (Nbhd i ∈ Tx ∧ x ∈ Nbhd i) (∃S1 : set, finite S1 ∧ S1 ⊆ (B i) ∧ ∀A : set, A ∈ (B i) → A ∩ Nbhd i ≠ Empty → A ∈ S1) Hprop).
An exact proof term for the current goal is (andER (Nbhd i ∈ Tx) (x ∈ Nbhd i) Hleft).
Set Nfam to be the term {v} ∪ {Nbhd i|i ∈ I}.
Set N0 to be the term intersection_of_family X Nfam.
We prove the intermediate claim HNfamPow: Nfam ∈ 𝒫 Tx.
Apply PowerI to the current goal.
Let W be given.
Assume HW: W ∈ Nfam.
We will prove W ∈ Tx.
Apply (binunionE' {v} {Nbhd i|i ∈ I} W (W ∈ Tx)) to the current goal.
Assume HWv: W ∈ {v}.
We prove the intermediate claim HWeq: W = v.
An exact proof term for the current goal is (SingE v W HWv).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HvTx.
Assume HWi: W ∈ {Nbhd i|i ∈ I}.
Apply (ReplE_impred I (λi0 : set ⇒ Nbhd i0) W HWi (W ∈ Tx)) to the current goal.
Let i be given.
Assume HiI: i ∈ I.
Assume HWeq: W = Nbhd i.
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is (HNbhdTx i HiI).
An exact proof term for the current goal is HW.
We prove the intermediate claim HNfamFin: finite Nfam.
We prove the intermediate claim HNrepFin: finite {Nbhd i|i ∈ I}.
An exact proof term for the current goal is (finite_Repl I HI_fin (λi0 : set ⇒ Nbhd i0)).
An exact proof term for the current goal is (binunion_finite {v} (Sing_finite v) {Nbhd i|i ∈ I} HNrepFin).
We prove the intermediate claim HN0Tx: N0 ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx Nfam HTx HNfamPow HNfamFin).
We prove the intermediate claim HxN0: x ∈ N0.
We will prove x ∈ intersection_of_family X Nfam.
We will prove x ∈ {x0 ∈ X|∀U : set, U ∈ Nfam → x0 ∈ U}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
Let W be given.
Assume HW: W ∈ Nfam.
We will prove x ∈ W.
Apply (binunionE' {v} {Nbhd i|i ∈ I} W (x ∈ W)) to the current goal.
Assume HWv: W ∈ {v}.
We prove the intermediate claim HWeq: W = v.
An exact proof term for the current goal is (SingE v W HWv).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is Hxv.
Assume HWi: W ∈ {Nbhd i|i ∈ I}.
Apply (ReplE_impred I (λi0 : set ⇒ Nbhd i0) W HWi (x ∈ W)) to the current goal.
Let i be given.
Assume HiI: i ∈ I.
Assume HWeq: W = Nbhd i.
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is (HNbhdx i HiI).
An exact proof term for the current goal is HW.
We use N0 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 HN0Tx.
An exact proof term for the current goal is HxN0.
Set GoodS to be the term λi : set ⇒ λS1 : set ⇒ finite S1 ∧ S1 ⊆ (B i) ∧ ∀A : set, A ∈ (B i) → A ∩ (Nbhd i) ≠ Empty → A ∈ S1.
Set Sof to be the term λi : set ⇒ Eps_i (GoodS i).
We prove the intermediate claim HSof: ∀i : set, i ∈ I → GoodS i (Sof i).
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim HNprop: GoodNbhd i (Nbhd i).
An exact proof term for the current goal is (HNbhd i HiI).
We prove the intermediate claim HexS1: ∃S1 : set, GoodS i S1.
An exact proof term for the current goal is (andER (Nbhd i ∈ Tx ∧ x ∈ Nbhd i) (∃S1 : set, finite S1 ∧ S1 ⊆ (B i) ∧ ∀A : set, A ∈ (B i) → A ∩ Nbhd i ≠ Empty → A ∈ S1) HNprop).
Apply HexS1 to the current goal.
Let S1 be given.
Assume HS1: GoodS i S1.
An exact proof term for the current goal is (Eps_i_ax (GoodS i) S1 HS1).
We prove the intermediate claim HSofFin: ∀i : set, i ∈ I → finite (Sof i).
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim Hprop: GoodS i (Sof i).
An exact proof term for the current goal is (HSof i HiI).
We prove the intermediate claim Hleft: finite (Sof i) ∧ (Sof i ⊆ (B i)).
An exact proof term for the current goal is (andEL (finite (Sof i) ∧ Sof i ⊆ (B i)) (∀A : set, A ∈ (B i) → A ∩ Nbhd i ≠ Empty → A ∈ (Sof i)) Hprop).
An exact proof term for the current goal is (andEL (finite (Sof i)) (Sof i ⊆ (B i)) Hleft).
Set Tset to be the term λi : set ⇒ {U0 ∖ Prev i|U0 ∈ (Sof i)}.
Set TFam to be the term {Tset i|i ∈ I}.
Set S0 to be the term ⋃ TFam.
We prove the intermediate claim HTsetFin: ∀i : set, i ∈ I → finite (Tset i).
Let i be given.
Assume HiI: i ∈ I.
An exact proof term for the current goal is (finite_Repl (Sof i) (HSofFin i HiI) (λU0 : set ⇒ U0 ∖ Prev i)).
We prove the intermediate claim HTFamFin: finite TFam.
An exact proof term for the current goal is (finite_Repl I HI_fin (λi0 : set ⇒ Tset i0)).
We prove the intermediate claim HS0Fin: finite S0.
We will prove finite (⋃ TFam).
Set p to be the term λF0 : set ⇒ (∀y : set, y ∈ F0 → finite y) → finite (⋃ F0).
We prove the intermediate claim Hp0: p Empty.
Assume _: ∀y : set, y ∈ Empty → finite y.
We will prove finite (⋃ Empty).
rewrite the current goal using Union_Empty_eq (from left to right).
An exact proof term for the current goal is finite_Empty.
We prove the intermediate claim HpStep: ∀F0 y : set, finite F0 → y ∉ F0 → p F0 → p (F0 ∪ {y}).
Let F0 and y be given.
Assume HF0fin: finite F0.
Assume HyNotin: y ∉ F0.
Assume IH: p F0.
Assume Hall: ∀z : set, z ∈ (F0 ∪ {y}) → finite z.
We prove the intermediate claim HallF0: ∀z : set, z ∈ F0 → finite z.
Let z be given.
Assume HzF0: z ∈ F0.
An exact proof term for the current goal is (Hall z (binunionI1 F0 {y} z HzF0)).
We prove the intermediate claim HFinY: finite y.
An exact proof term for the current goal is (Hall y (binunionI2 F0 {y} y (SingI y))).
We prove the intermediate claim HFinUF0: finite (⋃ F0).
An exact proof term for the current goal is (IH HallF0).
We will prove finite (⋃ (F0 ∪ {y})).
rewrite the current goal using (Union_binunion_singleton_eq F0 y) (from left to right).
An exact proof term for the current goal is (binunion_finite (⋃ F0) HFinUF0 y HFinY).
We prove the intermediate claim HpTFam: p TFam.
An exact proof term for the current goal is (finite_ind p Hp0 HpStep TFam HTFamFin).
We prove the intermediate claim HallTFam: ∀y : set, y ∈ TFam → finite y.
Let T be given.
Assume HT: T ∈ TFam.
Apply (ReplE_impred I (λi0 : set ⇒ Tset i0) T HT (finite T)) to the current goal.
Let i be given.
Assume HiI: i ∈ I.
Assume HTeq: T = Tset i.
rewrite the current goal using HTeq (from left to right).
An exact proof term for the current goal is (HTsetFin i HiI).
An exact proof term for the current goal is (HpTFam HallTFam).
We prove the intermediate claim HS0subC: S0 ⊆ C.
Let a be given.
Assume Ha: a ∈ S0.
Apply (UnionE_impred TFam a Ha (a ∈ C)) to the current goal.
Let T be given.
Assume HaT: a ∈ T.
Assume HT: T ∈ TFam.
Apply (ReplE_impred I (λi0 : set ⇒ Tset i0) T HT (a ∈ C)) to the current goal.
Let i be given.
Assume HiI: i ∈ I.
Assume HTeq: T = Tset i.
We prove the intermediate claim HaTi: a ∈ Tset i.
rewrite the current goal using HTeq (from right to left).
An exact proof term for the current goal is HaT.
Apply (ReplE_impred (Sof i) (λU0 : set ⇒ U0 ∖ Prev i) a HaTi (a ∈ C)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ (Sof i).
Assume Haeq: a = U0 ∖ Prev i.
We prove the intermediate claim HU0Bi: U0 ∈ (B i).
We prove the intermediate claim Hprop: GoodS i (Sof i).
An exact proof term for the current goal is (HSof i HiI).
We prove the intermediate claim Hleft: finite (Sof i) ∧ (Sof i ⊆ (B i)).
An exact proof term for the current goal is (andEL (finite (Sof i) ∧ Sof i ⊆ (B i)) (∀A : set, A ∈ (B i) → A ∩ Nbhd i ≠ Empty → A ∈ (Sof i)) Hprop).
We prove the intermediate claim Hsub: (Sof i) ⊆ (B i).
An exact proof term for the current goal is (andER (finite (Sof i)) (Sof i ⊆ (B i)) Hleft).
An exact proof term for the current goal is (Hsub U0 HU0).
We prove the intermediate claim HaCn: a ∈ Cn i.
rewrite the current goal using Haeq (from left to right).
An exact proof term for the current goal is (ReplI (B i) (λU1 : set ⇒ U1 ∖ Prev i) U0 HU0Bi).
We prove the intermediate claim HCnin: Cn i ∈ CFams.
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (HIomega i HiI).
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ Cn n0) i HiO).
An exact proof term for the current goal is (UnionI CFams a (Cn i) HaCn HCnin).
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 HS0Fin.
An exact proof term for the current goal is HS0subC.
Let A be given.
Assume HA: A ∈ C.
Assume HAnN: A ∩ N0 ≠ Empty.
We will prove A ∈ S0.
Apply (UnionE_impred CFams A HA (A ∈ S0)) to the current goal.
Let C0 be given.
Assume HA0: A ∈ C0.
Assume HC0: C0 ∈ CFams.
Apply (ReplE_impred ω (λn0 : set ⇒ Cn n0) C0 HC0 (A ∈ S0)) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume HC0eq: C0 = Cn i.
We prove the intermediate claim HAi: A ∈ Cn i.
rewrite the current goal using HC0eq (from right to left).
An exact proof term for the current goal is HA0.
Apply (ReplE_impred (B i) (λU1 : set ⇒ U1 ∖ Prev i) A HAi (A ∈ S0)) to the current goal.
Let U0 be given.
Assume HU0Bi: U0 ∈ (B i).
Assume Haeq: A = U0 ∖ Prev i.
We prove the intermediate claim Hexy: ∃y : set, y ∈ (A ∩ N0).
An exact proof term for the current goal is (nonempty_has_element (A ∩ N0) HAnN).
Apply Hexy to the current goal.
Let y be given.
Assume HyAn0: y ∈ (A ∩ N0).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE1 A N0 y HyAn0).
We prove the intermediate claim HyN0: y ∈ N0.
An exact proof term for the current goal is (binintersectE2 A N0 y HyAn0).
We prove the intermediate claim HyInt: y ∈ intersection_of_family X Nfam.
We will prove y ∈ intersection_of_family X Nfam.
An exact proof term for the current goal is HyN0.
We prove the intermediate claim HyAll: ∀W : set, W ∈ Nfam → y ∈ W.
An exact proof term for the current goal is (intersection_of_familyE2 X Nfam y HyInt).
We prove the intermediate claim HvNfam: v ∈ Nfam.
An exact proof term for the current goal is (binunionI1 {v} {Nbhd i0|i0 ∈ I} v (SingI v)).
We prove the intermediate claim Hyv: y ∈ v.
An exact proof term for the current goal is (HyAll v HvNfam).
We prove the intermediate claim HyUset: y ∈ U0 ∖ Prev i.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is HyA.
We prove the intermediate claim HyU0: y ∈ U0.
An exact proof term for the current goal is (setminusE1 U0 (Prev i) y HyUset).
We prove the intermediate claim HyNotPrev: y ∉ Prev i.
An exact proof term for the current goal is (setminusE2 U0 (Prev i) y HyUset).
We prove the intermediate claim HnotNini: ¬ (N ∈ i).
Assume HNini: N ∈ i.
We prove the intermediate claim HyVsetN: y ∈ Vset N.
We will prove y ∈ ⋃ (B N).
An exact proof term for the current goal is (UnionI (B N) y v Hyv HvBN).
We prove the intermediate claim HyPrev: y ∈ Prev i.
An exact proof term for the current goal is (famunionI i (λj : set ⇒ Vset j) N y HNini HyVsetN).
An exact proof term for the current goal is (HyNotPrev HyPrev).
We prove the intermediate claim HordN: ordinal N.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal N HNO).
We prove the intermediate claim Hordi: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i HiO).
We prove the intermediate claim HiI: i ∈ I.
Apply (ordinal_trichotomy_or_impred i N Hordi HordN (i ∈ I)) to the current goal.
Assume HiN: i ∈ N.
We prove the intermediate claim Hsub: N ⊆ I.
An exact proof term for the current goal is (ordsuccI1 N).
An exact proof term for the current goal is (Hsub i HiN).
Assume HiEq: i = N.
rewrite the current goal using HiEq (from left to right).
An exact proof term for the current goal is (ordsuccI2 N).
Assume HNini: N ∈ i.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotNini HNini).
We prove the intermediate claim HWi: (Nbhd i) ∈ Nfam.
We prove the intermediate claim HNbhdIn: (Nbhd i) ∈ {Nbhd j|j ∈ I}.
An exact proof term for the current goal is (ReplI I (λj : set ⇒ Nbhd j) i HiI).
An exact proof term for the current goal is (binunionI2 {v} {Nbhd j|j ∈ I} (Nbhd i) HNbhdIn).
We prove the intermediate claim HyNbhd: y ∈ Nbhd i.
An exact proof term for the current goal is (HyAll (Nbhd i) HWi).
We prove the intermediate claim HnonemptyUi: U0 ∩ (Nbhd i) ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (U0 ∩ (Nbhd i)) y (binintersectI U0 (Nbhd i) y HyU0 HyNbhd)).
We prove the intermediate claim HpropS: GoodS i (Sof i).
An exact proof term for the current goal is (HSof i HiI).
We prove the intermediate claim Hforall: ∀A0 : set, A0 ∈ (B i) → A0 ∩ (Nbhd i) ≠ Empty → A0 ∈ (Sof i).
An exact proof term for the current goal is (andER (finite (Sof i) ∧ Sof i ⊆ (B i)) (∀A0 : set, A0 ∈ (B i) → A0 ∩ (Nbhd i) ≠ Empty → A0 ∈ (Sof i)) HpropS).
We prove the intermediate claim HU0Sof: U0 ∈ (Sof i).
An exact proof term for the current goal is (Hforall U0 HU0Bi HnonemptyUi).
We prove the intermediate claim HAinTset: A ∈ Tset i.
rewrite the current goal using Haeq (from left to right).
An exact proof term for the current goal is (ReplI (Sof i) (λU1 : set ⇒ U1 ∖ Prev i) U0 HU0Sof).
We prove the intermediate claim HTsetIn: Tset i ∈ TFam.
An exact proof term for the current goal is (ReplI I (λi0 : set ⇒ Tset i0) i HiI).
An exact proof term for the current goal is (UnionI TFam A (Tset i) HAinTset HTsetIn).
We use C 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 HcovC.
An exact proof term for the current goal is HLF_C.
An exact proof term for the current goal is HrefCV.
∎