Let X and A be given.
Assume HA: finite_intersection_property X A.
We will prove ∃D : set, A ⊆ D ∧ maximal_finite_intersection_property X D.
We prove the intermediate claim HAsubPow: A ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (A ⊆ 𝒫 X) (∀F : set, finite F → F ⊆ A → intersection_of_family X F ≠ Empty) HA).
We prove the intermediate claim HAfip: ∀F : set, finite F → F ⊆ A → intersection_of_family X F ≠ Empty.
An exact proof term for the current goal is (andER (A ⊆ 𝒫 X) (∀F : set, finite F → F ⊆ A → intersection_of_family X F ≠ Empty) HA).
We prove the intermediate claim HexWO: ∃I : set, well_ordered_set I ∧ equip (𝒫 X) I.
An exact proof term for the current goal is (well_ordering_theorem_equip (𝒫 X)).
Apply HexWO to the current goal.
Let I be given.
Assume HI: well_ordered_set I ∧ equip (𝒫 X) 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 (𝒫 X) I) HI).
We prove the intermediate claim Hequip: equip (𝒫 X) I.
An exact proof term for the current goal is (andER (well_ordered_set I) (equip (𝒫 X) I) HI).
Apply Hequip to the current goal.
Let idx be given.
Assume Hbij: bij (𝒫 X) I idx.
We prove the intermediate claim HidxI: ∀U ∈ 𝒫 X, idx U ∈ I.
Apply (bijE (𝒫 X) I idx Hbij (∀U ∈ 𝒫 X, idx U ∈ I)) to the current goal.
Assume Hmap _Hinj _Hsurj.
An exact proof term for the current goal is Hmap.
We prove the intermediate claim HidxInj: ∀U V ∈ 𝒫 X, idx U = idx V → U = V.
Apply (bijE (𝒫 X) I idx Hbij (∀U V ∈ 𝒫 X, idx U = idx V → U = V)) to the current goal.
Assume _Hmap Hinj _Hsurj.
An exact proof term for the current goal is Hinj.
We prove the intermediate claim HidxSurj: ∀i ∈ I, ∃U ∈ 𝒫 X, idx U = i.
Apply (bijE (𝒫 X) I idx Hbij (∀i ∈ I, ∃U ∈ 𝒫 X, idx U = i)) to the current goal.
Assume _Hmap _Hinj Hsurj.
An exact proof term for the current goal is Hsurj.
Set pickP to be the term λi : set ⇒ Eps_i (λU : set ⇒ U ∈ 𝒫 X ∧ idx U = i).
We prove the intermediate claim HpickP: ∀i : set, i ∈ I → pickP i ∈ 𝒫 X ∧ idx (pickP i) = i.
Let i be given.
Assume Hi: i ∈ I.
We prove the intermediate claim HexU: ∃U : set, U ∈ 𝒫 X ∧ idx U = i.
An exact proof term for the current goal is (HidxSurj i Hi).
Apply HexU to the current goal.
Let U be given.
Assume HU: U ∈ 𝒫 X ∧ idx U = i.
An exact proof term for the current goal is (Eps_i_ax (λU0 : set ⇒ U0 ∈ 𝒫 X ∧ idx U0 = i) U HU).
We prove the intermediate claim HpickP_idx: ∀U : set, U ∈ 𝒫 X → pickP (idx U) = U.
Let U be given.
Assume HU: U ∈ 𝒫 X.
We prove the intermediate claim HiI: idx U ∈ I.
An exact proof term for the current goal is (HidxI U HU).
We prove the intermediate claim Hpick: pickP (idx U) ∈ 𝒫 X ∧ idx (pickP (idx U)) = idx U.
An exact proof term for the current goal is (HpickP (idx U) HiI).
We prove the intermediate claim HpPow: pickP (idx U) ∈ 𝒫 X.
An exact proof term for the current goal is (andEL (pickP (idx U) ∈ 𝒫 X) (idx (pickP (idx U)) = idx U) Hpick).
We prove the intermediate claim HidxEq: idx (pickP (idx U)) = idx U.
An exact proof term for the current goal is (andER (pickP (idx U) ∈ 𝒫 X) (idx (pickP (idx U)) = idx U) Hpick).
An exact proof term for the current goal is (HidxInj (pickP (idx U)) HpPow U HU HidxEq).
We prove the intermediate claim HIord: ordinal I.
An exact proof term for the current goal is (well_ordered_set_is_ordinal I HwoI).
We prove the intermediate claim HTrI: TransSet I.
An exact proof term for the current goal is (ordinal_TransSet I HIord).
We prove the intermediate claim HiSubI: ∀i : set, i ∈ I → i ⊆ I.
Let i be given.
Assume Hi: i ∈ I.
An exact proof term for the current goal is (HTrI i Hi).
Set Dof to be the term λSidx : set ⇒ A ∪ {pickP i|i ∈ Sidx}.
Set Fsel to be the term λS : set ⇒ λf : set → set ⇒ {i ∈ S|finite_intersection_property X (Dof (f i) ∪ {pickP i})}.
We prove the intermediate claim HFr: ∀S : set, ∀g h : set → set, (∀x ∈ S, g x = h x) → Fsel S g = Fsel S h.
Let S, g and h be given.
Assume Hgh: ∀x ∈ S, g x = h x.
Apply set_ext to the current goal.
Let i be given.
Assume Hi: i ∈ Fsel S g.
We will prove i ∈ Fsel S h.
We prove the intermediate claim HiS: i ∈ S.
An exact proof term for the current goal is (SepE1 S (λi0 : set ⇒ finite_intersection_property X (Dof (g i0) ∪ {pickP i0})) i Hi).
We prove the intermediate claim Hprop: finite_intersection_property X (Dof (g i) ∪ {pickP i}).
An exact proof term for the current goal is (SepE2 S (λi0 : set ⇒ finite_intersection_property X (Dof (g i0) ∪ {pickP i0})) i Hi).
We prove the intermediate claim Hgi: g i = h i.
An exact proof term for the current goal is (Hgh i HiS).
We prove the intermediate claim Hprop2: finite_intersection_property X (Dof (h i) ∪ {pickP i}).
rewrite the current goal using Hgi (from right to left).
An exact proof term for the current goal is Hprop.
An exact proof term for the current goal is (SepI S (λi0 : set ⇒ finite_intersection_property X (Dof (h i0) ∪ {pickP i0})) i HiS Hprop2).
Let i be given.
Assume Hi: i ∈ Fsel S h.
We will prove i ∈ Fsel S g.
We prove the intermediate claim HiS: i ∈ S.
An exact proof term for the current goal is (SepE1 S (λi0 : set ⇒ finite_intersection_property X (Dof (h i0) ∪ {pickP i0})) i Hi).
We prove the intermediate claim Hprop: finite_intersection_property X (Dof (h i) ∪ {pickP i}).
An exact proof term for the current goal is (SepE2 S (λi0 : set ⇒ finite_intersection_property X (Dof (h i0) ∪ {pickP i0})) i Hi).
We prove the intermediate claim Hgi: g i = h i.
An exact proof term for the current goal is (Hgh i HiS).
We prove the intermediate claim Hprop2: finite_intersection_property X (Dof (g i) ∪ {pickP i}).
rewrite the current goal using Hgi (from left to right).
An exact proof term for the current goal is Hprop.
An exact proof term for the current goal is (SepI S (λi0 : set ⇒ finite_intersection_property X (Dof (g i0) ∪ {pickP i0})) i HiS Hprop2).
Set Sel to be the term In_rec_i Fsel.
Set SI to be the term Sel I.
We prove the intermediate claim HSelEq: Sel I = Fsel I Sel.
An exact proof term for the current goal is (In_rec_i_eq Fsel HFr I).
We prove the intermediate claim HSelEqA: ∀S : set, Sel S = Fsel S Sel.
Let S be given.
An exact proof term for the current goal is (In_rec_i_eq Fsel HFr S).
We prove the intermediate claim HSIsubI: SI ⊆ I.
Let i be given.
Assume Hi: i ∈ SI.
We prove the intermediate claim HiF: i ∈ Fsel I Sel.
rewrite the current goal using HSelEq (from right to left).
An exact proof term for the current goal is Hi.
An exact proof term for the current goal is (SepE1 I (λi0 : set ⇒ finite_intersection_property X (Dof (Sel i0) ∪ {pickP i0})) i HiF).
We prove the intermediate claim HSelSub: ∀S : set, S ⊆ I → Sel S = SI ∩ S.
Let S be given.
Assume HSsubI: S ⊆ I.
Apply set_ext to the current goal.
Let i be given.
Assume Hi: i ∈ Sel S.
We will prove i ∈ SI ∩ S.
We prove the intermediate claim HSelS: Sel S = Fsel S Sel.
An exact proof term for the current goal is (HSelEqA S).
We prove the intermediate claim HiF: i ∈ Fsel S Sel.
rewrite the current goal using HSelS (from right to left).
An exact proof term for the current goal is Hi.
We prove the intermediate claim HiS: i ∈ S.
An exact proof term for the current goal is (SepE1 S (λi0 : set ⇒ finite_intersection_property X (Dof (Sel i0) ∪ {pickP i0})) i HiF).
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HSsubI i HiS).
We prove the intermediate claim Hprop: finite_intersection_property X (Dof (Sel i) ∪ {pickP i}).
An exact proof term for the current goal is (SepE2 S (λi0 : set ⇒ finite_intersection_property X (Dof (Sel i0) ∪ {pickP i0})) i HiF).
We prove the intermediate claim HiInSI: i ∈ SI.
We prove the intermediate claim HiFI: i ∈ Fsel I Sel.
An exact proof term for the current goal is (SepI I (λi0 : set ⇒ finite_intersection_property X (Dof (Sel i0) ∪ {pickP i0})) i HiI Hprop).
We prove the intermediate claim HSIDef: SI = Sel I.
Use reflexivity.
rewrite the current goal using HSIDef (from left to right).
rewrite the current goal using HSelEq (from left to right).
An exact proof term for the current goal is HiFI.
An exact proof term for the current goal is (binintersectI SI S i HiInSI HiS).
Let i be given.
Assume Hi: i ∈ SI ∩ S.
We will prove i ∈ Sel S.
We prove the intermediate claim HiSI: i ∈ SI.
An exact proof term for the current goal is (binintersectE1 SI S i Hi).
We prove the intermediate claim HiS: i ∈ S.
An exact proof term for the current goal is (binintersectE2 SI S i Hi).
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HSsubI i HiS).
We prove the intermediate claim HiFI: i ∈ Fsel I Sel.
rewrite the current goal using HSelEq (from right to left).
An exact proof term for the current goal is HiSI.
We prove the intermediate claim Hprop: finite_intersection_property X (Dof (Sel i) ∪ {pickP i}).
An exact proof term for the current goal is (SepE2 I (λi0 : set ⇒ finite_intersection_property X (Dof (Sel i0) ∪ {pickP i0})) i HiFI).
We prove the intermediate claim HiFS: i ∈ Fsel S Sel.
An exact proof term for the current goal is (SepI S (λi0 : set ⇒ finite_intersection_property X (Dof (Sel i0) ∪ {pickP i0})) i HiS Hprop).
We prove the intermediate claim Hsub: Fsel S Sel ⊆ Sel S.
We prove the intermediate claim HSelS: Sel S = Fsel S Sel.
An exact proof term for the current goal is (HSelEqA S).
rewrite the current goal using HSelS (from left to right).
An exact proof term for the current goal is (Subq_ref (Fsel S Sel)).
An exact proof term for the current goal is (Hsub i HiFS).
Set D to be the term Dof SI.
We use D to witness the existential quantifier.
Apply andI to the current goal.
Let U be given.
Assume HU: U ∈ A.
An exact proof term for the current goal is (binunionI1 A {pickP i|i ∈ SI} U HU).
We will prove finite_intersection_property X D ∧ ∀E : set, D ⊆ E → finite_intersection_property X E → E ⊆ D.
Apply andI to the current goal.
We will prove D ⊆ 𝒫 X ∧ ∀F : set, finite F → F ⊆ D → intersection_of_family X F ≠ Empty.
Apply andI to the current goal.
Let U be given.
Assume HU: U ∈ D.
Apply (binunionE' A {pickP i|i ∈ SI} U (U ∈ 𝒫 X)) to the current goal.
Assume HUA: U ∈ A.
An exact proof term for the current goal is (HAsubPow U HUA).
Assume HUSI: U ∈ {pickP i|i ∈ SI}.
Apply (ReplE_impred SI (λi0 : set ⇒ pickP i0) U HUSI (U ∈ 𝒫 X)) to the current goal.
Let i be given.
Assume HiSI: i ∈ SI.
Assume HUeq: U = pickP i.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HSIsubI i HiSI).
An exact proof term for the current goal is (andEL (pickP i ∈ 𝒫 X) (idx (pickP i) = i) (HpickP i HiI)).
An exact proof term for the current goal is HU.
Let F be given.
Assume HFfin: finite F.
Assume HFsubD: F ⊆ D.
Set Sidx to be the term {i ∈ SI|pickP i ∈ F}.
We prove the intermediate claim HSidxSubI: Sidx ⊆ I.
Let i be given.
Assume Hi: i ∈ Sidx.
We prove the intermediate claim HiSI: i ∈ SI.
An exact proof term for the current goal is (SepE1 SI (λi0 : set ⇒ pickP i0 ∈ F) i Hi).
An exact proof term for the current goal is (HSIsubI i HiSI).
We prove the intermediate claim HSidxFin: finite Sidx.
Set IdxF to be the term {idx U|U ∈ F}.
We prove the intermediate claim HIdxFfin: finite IdxF.
An exact proof term for the current goal is (Repl_finite idx F HFfin).
We prove the intermediate claim HSidxSubIdxF: Sidx ⊆ IdxF.
Let i be given.
Assume Hi: i ∈ Sidx.
We prove the intermediate claim HiSI: i ∈ SI.
An exact proof term for the current goal is (SepE1 SI (λi0 : set ⇒ pickP i0 ∈ F) i Hi).
We prove the intermediate claim HpInF: pickP i ∈ F.
An exact proof term for the current goal is (SepE2 SI (λi0 : set ⇒ pickP i0 ∈ F) i Hi).
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HSIsubI i HiSI).
We prove the intermediate claim HidxPi: idx (pickP i) = i.
An exact proof term for the current goal is (andER (pickP i ∈ 𝒫 X) (idx (pickP i) = i) (HpickP i HiI)).
rewrite the current goal using HidxPi (from right to left).
An exact proof term for the current goal is (ReplI F idx (pickP i) HpInF).
An exact proof term for the current goal is (Subq_finite IdxF HIdxFfin Sidx HSidxSubIdxF).
Apply (xm (Sidx = Empty)) to the current goal.
Assume HSidx0: Sidx = Empty.
We prove the intermediate claim HFsubA: F ⊆ A.
Let U be given.
Assume HUF: U ∈ F.
We prove the intermediate claim HUD: U ∈ D.
An exact proof term for the current goal is (HFsubD U HUF).
Apply (binunionE' A {pickP i|i ∈ SI} U (U ∈ A)) to the current goal.
Assume HUA: U ∈ A.
An exact proof term for the current goal is HUA.
Assume HUpick: U ∈ {pickP i|i ∈ SI}.
Apply FalseE to the current goal.
Apply (ReplE_impred SI (λi0 : set ⇒ pickP i0) U HUpick (False)) to the current goal.
Let i be given.
Assume HiSI: i ∈ SI.
Assume HUeq: U = pickP i.
We prove the intermediate claim HiSidx: i ∈ Sidx.
We prove the intermediate claim HpInF: pickP i ∈ F.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HUF.
An exact proof term for the current goal is (SepI SI (λi0 : set ⇒ pickP i0 ∈ F) i HiSI HpInF).
We prove the intermediate claim Hi0: i ∈ Empty.
rewrite the current goal using HSidx0 (from right to left).
An exact proof term for the current goal is HiSidx.
An exact proof term for the current goal is (EmptyE i Hi0).
An exact proof term for the current goal is HUD.
An exact proof term for the current goal is (HAfip F HFfin HFsubA).
Assume HSidxNe: ¬ (Sidx = Empty).
We prove the intermediate claim Hexm: ∃m : set, m ∈ Sidx ∧ ∀s : set, s ∈ Sidx → s ⊆ m.
An exact proof term for the current goal is (finite_nonempty_subset_of_ordinal_has_max I Sidx HIord HSidxFin HSidxSubI HSidxNe).
Apply Hexm to the current goal.
Let m be given.
Assume Hm: m ∈ Sidx ∧ ∀s : set, s ∈ Sidx → s ⊆ m.
We prove the intermediate claim HmSidx: m ∈ Sidx.
An exact proof term for the current goal is (andEL (m ∈ Sidx) (∀s : set, s ∈ Sidx → s ⊆ m) Hm).
We prove the intermediate claim HmMax: ∀s : set, s ∈ Sidx → s ⊆ m.
An exact proof term for the current goal is (andER (m ∈ Sidx) (∀s : set, s ∈ Sidx → s ⊆ m) Hm).
We prove the intermediate claim HmSI: m ∈ SI.
An exact proof term for the current goal is (SepE1 SI (λi0 : set ⇒ pickP i0 ∈ F) m HmSidx).
We prove the intermediate claim HpmInF: pickP m ∈ F.
An exact proof term for the current goal is (SepE2 SI (λi0 : set ⇒ pickP i0 ∈ F) m HmSidx).
We prove the intermediate claim HmI: m ∈ I.
An exact proof term for the current goal is (HSIsubI m HmSI).
We prove the intermediate claim HmSubI: m ⊆ I.
An exact proof term for the current goal is (HiSubI m HmI).
We prove the intermediate claim HSelm: Sel m = SI ∩ m.
An exact proof term for the current goal is (HSelSub m HmSubI).
We prove the intermediate claim HmFI: m ∈ Fsel I Sel.
rewrite the current goal using HSelEq (from right to left).
An exact proof term for the current goal is HmSI.
We prove the intermediate claim HmFIP: finite_intersection_property X (Dof (Sel m) ∪ {pickP m}).
An exact proof term for the current goal is (SepE2 I (λi0 : set ⇒ finite_intersection_property X (Dof (Sel i0) ∪ {pickP i0})) m HmFI).
We prove the intermediate claim HFsubEm: F ⊆ Dof (Sel m) ∪ {pickP m}.
Let U be given.
Assume HUF: U ∈ F.
We prove the intermediate claim HUd: U ∈ D.
An exact proof term for the current goal is (HFsubD U HUF).
Apply (binunionE' A {pickP i|i ∈ SI} U (U ∈ (Dof (Sel m) ∪ {pickP m}))) to the current goal.
Assume HUA: U ∈ A.
An exact proof term for the current goal is (binunionI1 (Dof (Sel m)) {pickP m} U (binunionI1 A {pickP i|i ∈ Sel m} U HUA)).
Assume HUpick: U ∈ {pickP i|i ∈ SI}.
Apply (ReplE_impred SI (λi0 : set ⇒ pickP i0) U HUpick (U ∈ (Dof (Sel m) ∪ {pickP m}))) to the current goal.
Let i be given.
Assume HiSI: i ∈ SI.
Assume HUeq: U = pickP i.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HiSidx: i ∈ Sidx.
We prove the intermediate claim HpInF: pickP i ∈ F.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HUF.
An exact proof term for the current goal is (SepI SI (λi0 : set ⇒ pickP i0 ∈ F) i HiSI HpInF).
We prove the intermediate claim Himax: i ⊆ m.
An exact proof term for the current goal is (HmMax i HiSidx).
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HSIsubI i HiSI).
Apply (xm (i = m)) to the current goal.
Assume Hieq: i = m.
rewrite the current goal using Hieq (from left to right).
An exact proof term for the current goal is (binunionI2 (Dof (Sel m)) {pickP m} (pickP m) (SingI (pickP m))).
Assume Hineq: ¬ (i = m).
We prove the intermediate claim HiInm: i ∈ m.
Apply (ordinal_trichotomy_or_impred i m (ordinal_Hered I HIord i HiI) (ordinal_Hered I HIord m HmI) (i ∈ m)) to the current goal.
Assume Him: i ∈ m.
An exact proof term for the current goal is Him.
Assume Hieq: i = m.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hineq Hieq).
Assume Hmi: m ∈ i.
Apply FalseE to the current goal.
We prove the intermediate claim HmSub: m ⊆ i.
We prove the intermediate claim Hiord: ordinal i.
An exact proof term for the current goal is (ordinal_Hered I HIord i HiI).
We prove the intermediate claim Htri: TransSet i.
An exact proof term for the current goal is (ordinal_TransSet i Hiord).
An exact proof term for the current goal is (Htri m Hmi).
We prove the intermediate claim Hmi2: i ⊆ m.
An exact proof term for the current goal is Himax.
We prove the intermediate claim Heq: i = m.
Apply set_ext to the current goal.
An exact proof term for the current goal is Hmi2.
An exact proof term for the current goal is HmSub.
An exact proof term for the current goal is (Hineq Heq).
We prove the intermediate claim HiSelm: i ∈ Sel m.
rewrite the current goal using HSelm (from left to right).
An exact proof term for the current goal is (binintersectI SI m i HiSI HiInm).
An exact proof term for the current goal is (binunionI1 (Dof (Sel m)) {pickP m} (pickP i) (binunionI2 A {pickP j|j ∈ Sel m} (pickP i) (ReplI (Sel m) (λj0 : set ⇒ pickP j0) i HiSelm))).
An exact proof term for the current goal is HUd.
We prove the intermediate claim HmFIP2: ∀F0 : set, finite F0 → F0 ⊆ (Dof (Sel m) ∪ {pickP m}) → intersection_of_family X F0 ≠ Empty.
An exact proof term for the current goal is (andER ((Dof (Sel m) ∪ {pickP m}) ⊆ 𝒫 X) (∀F0 : set, finite F0 → F0 ⊆ (Dof (Sel m) ∪ {pickP m}) → intersection_of_family X F0 ≠ Empty) HmFIP).
An exact proof term for the current goal is (HmFIP2 F HFfin HFsubEm).
Let E be given.
Assume HDE: D ⊆ E.
Assume HEfip: finite_intersection_property X E.
We will prove E ⊆ D.
Let U be given.
Assume HU: U ∈ E.
We prove the intermediate claim HESubPow: E ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (E ⊆ 𝒫 X) (∀F : set, finite F → F ⊆ E → intersection_of_family X F ≠ Empty) HEfip).
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (HESubPow U HU).
Set i to be the term idx U.
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HidxI U HUpow).
We prove the intermediate claim HUeq: pickP i = U.
We prove the intermediate claim Hidef: i = idx U.
Use reflexivity.
rewrite the current goal using Hidef (from left to right).
An exact proof term for the current goal is (HpickP_idx U HUpow).
Set DU to be the term D ∪ {U}.
We prove the intermediate claim HDUsubE: DU ⊆ E.
Let V be given.
Assume HV: V ∈ DU.
Apply (binunionE' D {U} V (V ∈ E)) to the current goal.
Assume HVD: V ∈ D.
An exact proof term for the current goal is (HDE V HVD).
Assume HVU: V ∈ {U}.
We prove the intermediate claim HVeq: V = U.
An exact proof term for the current goal is (SingE U V HVU).
rewrite the current goal using HVeq (from left to right).
An exact proof term for the current goal is HU.
An exact proof term for the current goal is HV.
We prove the intermediate claim HfipDU: finite_intersection_property X DU.
We prove the intermediate claim HDUpow: DU ⊆ 𝒫 X.
Let V be given.
Assume HV: V ∈ DU.
An exact proof term for the current goal is (HESubPow V (HDUsubE V HV)).
We will prove DU ⊆ 𝒫 X ∧ ∀F : set, finite F → F ⊆ DU → intersection_of_family X F ≠ Empty.
Apply andI to the current goal.
An exact proof term for the current goal is HDUpow.
Let F be given.
Assume HFfin: finite F.
Assume HFsub: F ⊆ DU.
Apply HEfip to the current goal.
Assume _Hpow HFip.
An exact proof term for the current goal is (HFip F HFfin (λV HVF ⇒ HDUsubE V (HFsub V HVF))).
We prove the intermediate claim HSelSubi: Sel i = SI ∩ i.
An exact proof term for the current goal is (HSelSub i (HiSubI i HiI)).
We prove the intermediate claim HDofSubD: Dof (Sel i) ⊆ D.
Let V be given.
Assume HV: V ∈ Dof (Sel i).
Apply (binunionE' A {pickP j|j ∈ Sel i} V (V ∈ D)) to the current goal.
Assume HVA: V ∈ A.
An exact proof term for the current goal is (binunionI1 A {pickP j|j ∈ SI} V HVA).
Assume HVsel: V ∈ {pickP j|j ∈ Sel i}.
Apply (ReplE_impred (Sel i) (λj0 : set ⇒ pickP j0) V HVsel (V ∈ D)) to the current goal.
Let j be given.
Assume Hj: j ∈ Sel i.
Assume HVeq: V = pickP j.
rewrite the current goal using HVeq (from left to right).
We prove the intermediate claim HjSI: j ∈ SI.
We prove the intermediate claim Hj2: j ∈ SI ∩ i.
rewrite the current goal using HSelSubi (from right to left).
An exact proof term for the current goal is Hj.
An exact proof term for the current goal is (binintersectE1 SI i j Hj2).
An exact proof term for the current goal is (binunionI2 A {pickP j0|j0 ∈ SI} (pickP j) (ReplI SI (λj0 : set ⇒ pickP j0) j HjSI)).
An exact proof term for the current goal is HV.
We prove the intermediate claim HfipTest: finite_intersection_property X (Dof (Sel i) ∪ {pickP i}).
We prove the intermediate claim HSub: (Dof (Sel i) ∪ {pickP i}) ⊆ DU.
Let V be given.
Assume HV: V ∈ Dof (Sel i) ∪ {pickP i}.
Apply (binunionE' (Dof (Sel i)) {pickP i} V (V ∈ DU)) to the current goal.
Assume HV0: V ∈ Dof (Sel i).
An exact proof term for the current goal is (binunionI1 D {U} V (HDofSubD V HV0)).
Assume HV1: V ∈ {pickP i}.
We prove the intermediate claim HVeq: V = pickP i.
An exact proof term for the current goal is (SingE (pickP i) V HV1).
rewrite the current goal using HVeq (from left to right).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binunionI2 D {U} U (SingI U)).
An exact proof term for the current goal is HV.
We will prove (Dof (Sel i) ∪ {pickP i}) ⊆ 𝒫 X ∧ ∀F : set, finite F → F ⊆ (Dof (Sel i) ∪ {pickP i}) → intersection_of_family X F ≠ Empty.
Apply andI to the current goal.
Let V be given.
Assume HV: V ∈ Dof (Sel i) ∪ {pickP i}.
An exact proof term for the current goal is (andEL (DU ⊆ 𝒫 X) (∀F : set, finite F → F ⊆ DU → intersection_of_family X F ≠ Empty) HfipDU V (HSub V HV)).
Let F be given.
Assume HFfin: finite F.
Assume HFsub: F ⊆ Dof (Sel i) ∪ {pickP i}.
Apply HfipDU to the current goal.
Assume _ HDUfip.
An exact proof term for the current goal is (HDUfip F HFfin (λV HVF ⇒ HSub V (HFsub V HVF))).
We prove the intermediate claim HiSelI: i ∈ SI.
We prove the intermediate claim HiFI: i ∈ Fsel I Sel.
An exact proof term for the current goal is (SepI I (λi0 : set ⇒ finite_intersection_property X (Dof (Sel i0) ∪ {pickP i0})) i HiI HfipTest).
We prove the intermediate claim HSIDef: SI = Sel I.
Use reflexivity.
rewrite the current goal using HSIDef (from left to right).
rewrite the current goal using HSelEq (from left to right).
An exact proof term for the current goal is HiFI.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is (binunionI2 A {pickP j|j ∈ SI} (pickP i) (ReplI SI (λj0 : set ⇒ pickP j0) i HiSelI)).
∎