Let X, d, Y and n be given.
Assume Hm: metric_on X d.
Assume HnO: n ∈ ω.
Assume HYsubX: Y ⊆ X.
We will prove ∃S : set, maximal_eps_separated_set_on X d Y S n.
We prove the intermediate claim HexWO: ∃I : set, well_ordered_set I ∧ equip Y I.
An exact proof term for the current goal is (well_ordering_theorem_equip Y).
Apply HexWO to the current goal.
Let I be given.
Assume HI: well_ordered_set I ∧ equip Y I.
We prove the intermediate claim HeqYI: equip Y I.
An exact proof term for the current goal is (andER (well_ordered_set I) (equip Y I) HI).
Apply HeqYI to the current goal.
Let idx be given.
Assume Hbij: bij Y I idx.
We prove the intermediate claim HidxSurj: ∀i : set, i ∈ I → ∃y : set, y ∈ Y ∧ idx y = i.
Apply (bijE Y I idx Hbij (∀i : set, i ∈ I → ∃y : set, y ∈ Y ∧ idx y = i)) to the current goal.
Assume _Hmap _Hinj _Hsurj.
An exact proof term for the current goal is _Hsurj.
Set pickY to be the term λi : set ⇒ Eps_i (λy : set ⇒ y ∈ Y ∧ idx y = i).
We prove the intermediate claim HpickY: ∀i : set, i ∈ I → pickY i ∈ Y ∧ idx (pickY i) = i.
Let i be given.
Assume Hi: i ∈ I.
We prove the intermediate claim Hexy: ∃y : set, y ∈ Y ∧ idx y = i.
An exact proof term for the current goal is (HidxSurj i Hi).
Apply Hexy to the current goal.
Let y be given.
Assume Hy: y ∈ Y ∧ idx y = i.
An exact proof term for the current goal is (Eps_i_ax (λy0 : set ⇒ y0 ∈ Y ∧ idx y0 = i) y Hy).
Set Fsel to be the term λA : set ⇒ λf : set → set ⇒ {i ∈ A|∀j : set, j ∈ f i → ¬ (Rlt (apply_fun d (pickY i,pickY j)) (eps_ n))}.
We prove the intermediate claim HFr: ∀A : set, ∀g h : set → set, (∀x ∈ A, g x = h x) → Fsel A g = Fsel A h.
Let A, g and h be given.
Assume Hgh: ∀x ∈ A, g x = h x.
Apply set_ext to the current goal.
Let i be given.
Assume Hi: i ∈ Fsel A g.
We will prove i ∈ Fsel A h.
We prove the intermediate claim HiA: i ∈ A.
An exact proof term for the current goal is (SepE1 A (λi0 : set ⇒ ∀j : set, j ∈ g i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i Hi).
We prove the intermediate claim Hprop: ∀j : set, j ∈ g i → ¬ (Rlt (apply_fun d (pickY i,pickY j)) (eps_ n)).
An exact proof term for the current goal is (SepE2 A (λi0 : set ⇒ ∀j : set, j ∈ g i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i Hi).
We prove the intermediate claim HgiEq: g i = h i.
An exact proof term for the current goal is (Hgh i HiA).
We prove the intermediate claim HdefF: Fsel A h = {i0 ∈ A|∀j : set, j ∈ h i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
Use reflexivity.
rewrite the current goal using HdefF (from left to right).
We prove the intermediate claim Hprop2: ∀j : set, j ∈ h i → ¬ (Rlt (apply_fun d (pickY i,pickY j)) (eps_ n)).
Let j be given.
Assume Hj: j ∈ h i.
We prove the intermediate claim Hjg: j ∈ g i.
rewrite the current goal using HgiEq (from left to right).
An exact proof term for the current goal is Hj.
An exact proof term for the current goal is (Hprop j Hjg).
An exact proof term for the current goal is (SepI A (λi0 : set ⇒ ∀j : set, j ∈ h i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i HiA Hprop2).
Let i be given.
Assume Hi: i ∈ Fsel A h.
We will prove i ∈ Fsel A g.
We prove the intermediate claim HiA: i ∈ A.
An exact proof term for the current goal is (SepE1 A (λi0 : set ⇒ ∀j : set, j ∈ h i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i Hi).
We prove the intermediate claim Hprop: ∀j : set, j ∈ h i → ¬ (Rlt (apply_fun d (pickY i,pickY j)) (eps_ n)).
An exact proof term for the current goal is (SepE2 A (λi0 : set ⇒ ∀j : set, j ∈ h i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i Hi).
We prove the intermediate claim HgiEq: g i = h i.
An exact proof term for the current goal is (Hgh i HiA).
We prove the intermediate claim HdefF: Fsel A g = {i0 ∈ A|∀j : set, j ∈ g i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
Use reflexivity.
rewrite the current goal using HdefF (from left to right).
We prove the intermediate claim Hprop2: ∀j : set, j ∈ g i → ¬ (Rlt (apply_fun d (pickY i,pickY j)) (eps_ n)).
Let j be given.
Assume Hj: j ∈ g i.
We prove the intermediate claim Hjh: j ∈ h i.
rewrite the current goal using HgiEq (from right to left).
An exact proof term for the current goal is Hj.
An exact proof term for the current goal is (Hprop j Hjh).
An exact proof term for the current goal is (SepI A (λi0 : set ⇒ ∀j : set, j ∈ g i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i HiA Hprop2).
Set Sel to be the term In_rec_i Fsel.
Set SI to be the term Sel I.
Set S to be the term {pickY i|i ∈ SI}.
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 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.
We prove the intermediate claim HdefF: Fsel I Sel = {i0 ∈ I|∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
Use reflexivity.
We prove the intermediate claim HiSep: i ∈ {i0 ∈ I|∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
rewrite the current goal using HdefF (from right to left).
An exact proof term for the current goal is HiF.
An exact proof term for the current goal is (SepE1 I (λi0 : set ⇒ ∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i HiSep).
We prove the intermediate claim HSsubY: S ⊆ Y.
Let y be given.
Assume Hy: y ∈ S.
Apply (ReplE_impred SI (λi0 : set ⇒ pickY i0) y Hy (y ∈ Y)) to the current goal.
Let i be given.
Assume Hi: i ∈ SI.
Assume Heq: y = pickY i.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HSIsubI i Hi).
An exact proof term for the current goal is (andEL (pickY i ∈ Y) (idx (pickY i) = i) (HpickY i HiI)).
We prove the intermediate claim HSelEqA: ∀A : set, Sel A = Fsel A Sel.
Let A be given.
An exact proof term for the current goal is (In_rec_i_eq Fsel HFr A).
We prove the intermediate claim HSelSub: ∀A : set, A ⊆ I → Sel A = SI ∩ A.
Let A be given.
Assume HA: A ⊆ I.
Apply set_ext to the current goal.
Let i be given.
Assume Hi: i ∈ Sel A.
We will prove i ∈ SI ∩ A.
We prove the intermediate claim HSelA: Sel A = Fsel A Sel.
An exact proof term for the current goal is (HSelEqA A).
We prove the intermediate claim HiF: i ∈ Fsel A Sel.
rewrite the current goal using HSelA (from right to left).
An exact proof term for the current goal is Hi.
We prove the intermediate claim HdefF: Fsel A Sel = {i0 ∈ A|∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
Use reflexivity.
We prove the intermediate claim HiSep: i ∈ {i0 ∈ A|∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
rewrite the current goal using HdefF (from right to left).
An exact proof term for the current goal is HiF.
We prove the intermediate claim HiA: i ∈ A.
An exact proof term for the current goal is (SepE1 A (λi0 : set ⇒ ∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i HiSep).
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HA i HiA).
We prove the intermediate claim Hfar: ∀j : set, j ∈ Sel i → ¬ (Rlt (apply_fun d (pickY i,pickY j)) (eps_ n)).
An exact proof term for the current goal is (SepE2 A (λi0 : set ⇒ ∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i HiSep).
We prove the intermediate claim HiFI: i ∈ Fsel I Sel.
An exact proof term for the current goal is (SepI I (λi0 : set ⇒ ∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i HiI Hfar).
We prove the intermediate claim HiSI: i ∈ SI.
We prove the intermediate claim HiSelI: i ∈ Sel I.
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 HiSelI.
An exact proof term for the current goal is (binintersectI SI A i HiSI HiA).
Let i be given.
Assume Hi: i ∈ SI ∩ A.
We will prove i ∈ Sel A.
We prove the intermediate claim HiSI: i ∈ SI.
An exact proof term for the current goal is (binintersectE1 SI A i Hi).
We prove the intermediate claim HiA: i ∈ A.
An exact proof term for the current goal is (binintersectE2 SI A i Hi).
We prove the intermediate claim HSelA: Sel A = Fsel A Sel.
An exact proof term for the current goal is (HSelEqA A).
rewrite the current goal using HSelA (from left to right).
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 HdefFI: Fsel I Sel = {i0 ∈ I|∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
Use reflexivity.
We prove the intermediate claim HiSepI: i ∈ {i0 ∈ I|∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
rewrite the current goal using HdefFI (from right to left).
An exact proof term for the current goal is HiFI.
We prove the intermediate claim Hfar: ∀j : set, j ∈ Sel i → ¬ (Rlt (apply_fun d (pickY i,pickY j)) (eps_ n)).
An exact proof term for the current goal is (SepE2 I (λi0 : set ⇒ ∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i HiSepI).
We prove the intermediate claim HdefF: Fsel A Sel = {i0 ∈ A|∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))}.
Use reflexivity.
rewrite the current goal using HdefF (from left to right).
An exact proof term for the current goal is (SepI A (λi0 : set ⇒ ∀j : set, j ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY j)) (eps_ n))) i HiA Hfar).
We use S to witness the existential quantifier.
We will prove maximal_eps_separated_set_on X d Y S n.
We prove the intermediate claim HdefMax: maximal_eps_separated_set_on X d Y S n = ((Y ⊆ X) ∧ (S ⊆ Y) ∧ (∀x y : set, x ∈ S → y ∈ S → ¬ (x = y) → ¬ (Rlt (apply_fun d (x,y)) (eps_ n))) ∧ (∀x : set, x ∈ Y → (∀y : set, y ∈ S → ¬ (Rlt (apply_fun d (x,y)) (eps_ n))) → x ∈ S)).
Use reflexivity.
rewrite the current goal using HdefMax (from left to right).
Apply and4I to the current goal.
An exact proof term for the current goal is HYsubX.
An exact proof term for the current goal is HSsubY.
Let x and y be given.
Assume HxS: x ∈ S.
Assume HyS: y ∈ S.
Assume HxyNe: ¬ (x = y).
We will prove ¬ (Rlt (apply_fun d (x,y)) (eps_ n)).
Assume Hltxy: Rlt (apply_fun d (x,y)) (eps_ n).
We will prove False.
Apply (ReplE_impred SI (λi0 : set ⇒ pickY i0) x HxS False) to the current goal.
Let i be given.
Assume HiSI: i ∈ SI.
Assume HxEq: x = pickY i.
Apply (ReplE_impred SI (λj0 : set ⇒ pickY j0) y HyS False) to the current goal.
Let j be given.
Assume HjSI: j ∈ SI.
Assume HyEq: y = pickY j.
We prove the intermediate claim Hltij: Rlt (apply_fun d (pickY i,pickY j)) (eps_ n).
rewrite the current goal using HxEq (from right to left).
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is Hltxy.
We prove the intermediate claim HijNe: ¬ (i = j).
Assume Hij: i = j.
Apply HxyNe to the current goal.
rewrite the current goal using HxEq (from left to right).
rewrite the current goal using HyEq (from left to right).
rewrite the current goal using Hij (from left to right).
Use reflexivity.
We prove the intermediate claim Hwell: well_ordered_set I.
An exact proof term for the current goal is (andEL (well_ordered_set I) (equip Y I) HI).
We prove the intermediate claim HIord: ordinal I.
An exact proof term for the current goal is (well_ordered_set_is_ordinal I Hwell).
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 HjI: j ∈ I.
An exact proof term for the current goal is (HSIsubI j HjSI).
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 HjOrd: ordinal j.
An exact proof term for the current goal is (ordinal_Hered I HIord j HjI).
We prove the intermediate claim HpiY: pickY i ∈ Y.
An exact proof term for the current goal is (andEL (pickY i ∈ Y) (idx (pickY i) = i) (HpickY i HiI)).
We prove the intermediate claim HpjY: pickY j ∈ Y.
An exact proof term for the current goal is (andEL (pickY j ∈ Y) (idx (pickY j) = j) (HpickY j HjI)).
We prove the intermediate claim HpiX: pickY i ∈ X.
An exact proof term for the current goal is (HYsubX (pickY i) HpiY).
We prove the intermediate claim HpjX: pickY j ∈ X.
An exact proof term for the current goal is (HYsubX (pickY j) HpjY).
Apply (ordinal_trichotomy_or_impred i j HiOrd HjOrd False) to the current goal.
Assume Hij: i ∈ j.
We prove the intermediate claim HtransI: TransSet I.
An exact proof term for the current goal is (ordinal_TransSet I HIord).
We prove the intermediate claim HjSubI: j ⊆ I.
An exact proof term for the current goal is (HtransI j HjI).
We prove the intermediate claim HSelj: Sel j = SI ∩ j.
An exact proof term for the current goal is (HSelSub j HjSubI).
We prove the intermediate claim HiSelj: i ∈ Sel j.
rewrite the current goal using HSelj (from left to right).
An exact proof term for the current goal is (binintersectI SI j i HiSI Hij).
We prove the intermediate claim HjFI: j ∈ Fsel I Sel.
rewrite the current goal using HSelEq (from right to left).
An exact proof term for the current goal is HjSI.
We prove the intermediate claim HdefFI: Fsel I Sel = {i0 ∈ I|∀k : set, k ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY k)) (eps_ n))}.
Use reflexivity.
We prove the intermediate claim HjSep: j ∈ {i0 ∈ I|∀k : set, k ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY k)) (eps_ n))}.
rewrite the current goal using HdefFI (from right to left).
An exact proof term for the current goal is HjFI.
We prove the intermediate claim HjFar: ∀k : set, k ∈ Sel j → ¬ (Rlt (apply_fun d (pickY j,pickY k)) (eps_ n)).
An exact proof term for the current goal is (SepE2 I (λi0 : set ⇒ ∀k : set, k ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY k)) (eps_ n))) j HjSep).
We prove the intermediate claim Hltji: Rlt (apply_fun d (pickY j,pickY i)) (eps_ n).
We prove the intermediate claim Hsymji: apply_fun d (pickY j,pickY i) = apply_fun d (pickY i,pickY j).
An exact proof term for the current goal is (metric_on_symmetric X d (pickY j) (pickY i) Hm HpjX HpiX).
rewrite the current goal using Hsymji (from left to right).
An exact proof term for the current goal is Hltij.
An exact proof term for the current goal is ((HjFar i HiSelj) Hltji).
Assume Hij: i = j.
An exact proof term for the current goal is (HijNe Hij).
Assume Hji: j ∈ i.
We prove the intermediate claim HtransI: TransSet I.
An exact proof term for the current goal is (ordinal_TransSet I HIord).
We prove the intermediate claim HiSubI: i ⊆ I.
An exact proof term for the current goal is (HtransI i HiI).
We prove the intermediate claim HSeli: Sel i = SI ∩ i.
An exact proof term for the current goal is (HSelSub i HiSubI).
We prove the intermediate claim HjSeli: j ∈ Sel i.
rewrite the current goal using HSeli (from left to right).
An exact proof term for the current goal is (binintersectI SI i j HjSI Hji).
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 HdefFI: Fsel I Sel = {i0 ∈ I|∀k : set, k ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY k)) (eps_ n))}.
Use reflexivity.
We prove the intermediate claim HiSep: i ∈ {i0 ∈ I|∀k : set, k ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY k)) (eps_ n))}.
rewrite the current goal using HdefFI (from right to left).
An exact proof term for the current goal is HiFI.
We prove the intermediate claim HiFar: ∀k : set, k ∈ Sel i → ¬ (Rlt (apply_fun d (pickY i,pickY k)) (eps_ n)).
An exact proof term for the current goal is (SepE2 I (λi0 : set ⇒ ∀k : set, k ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY k)) (eps_ n))) i HiSep).
An exact proof term for the current goal is ((HiFar j HjSeli) Hltij).
Let x be given.
Assume HxY: x ∈ Y.
Assume HfarS: ∀y : set, y ∈ S → ¬ (Rlt (apply_fun d (x,y)) (eps_ n)).
We will prove x ∈ S.
We prove the intermediate claim HidxMap: ∀u ∈ Y, idx u ∈ I.
Apply (bijE Y I idx Hbij (∀u ∈ Y, idx u ∈ I)) to the current goal.
Assume Hmap _ _.
An exact proof term for the current goal is Hmap.
We prove the intermediate claim HidxInj: ∀u v ∈ Y, idx u = idx v → u = v.
Apply (bijE Y I idx Hbij (∀u v ∈ Y, idx u = idx v → u = v)) to the current goal.
Assume _ Hinj _.
An exact proof term for the current goal is Hinj.
Set i to be the term idx x.
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (HidxMap x HxY).
We prove the intermediate claim HpiY: pickY i ∈ Y.
An exact proof term for the current goal is (andEL (pickY i ∈ Y) (idx (pickY i) = i) (HpickY i HiI)).
We prove the intermediate claim HidxPick: idx (pickY i) = i.
An exact proof term for the current goal is (andER (pickY i ∈ Y) (idx (pickY i) = i) (HpickY i HiI)).
We prove the intermediate claim HpiEq: pickY i = x.
Apply (HidxInj (pickY i) HpiY x HxY) to the current goal.
An exact proof term for the current goal is HidxPick.
We prove the intermediate claim HIord: ordinal I.
An exact proof term for the current goal is (well_ordered_set_is_ordinal I (andEL (well_ordered_set I) (equip Y I) HI)).
We prove the intermediate claim HtransI: TransSet I.
An exact proof term for the current goal is (ordinal_TransSet I HIord).
We prove the intermediate claim HiSubI: i ⊆ I.
An exact proof term for the current goal is (HtransI i HiI).
We prove the intermediate claim HSeli: Sel i = SI ∩ i.
An exact proof term for the current goal is (HSelSub i HiSubI).
We prove the intermediate claim HfarSel: ∀j : set, j ∈ Sel i → ¬ (Rlt (apply_fun d (pickY i,pickY j)) (eps_ n)).
Let j be given.
Assume HjSel: j ∈ Sel i.
We prove the intermediate claim HjInt: j ∈ SI ∩ i.
rewrite the current goal using HSeli (from right to left).
An exact proof term for the current goal is HjSel.
We prove the intermediate claim HjSI: j ∈ SI.
An exact proof term for the current goal is (binintersectE1 SI i j HjInt).
We prove the intermediate claim HjyS: pickY j ∈ S.
An exact proof term for the current goal is (ReplI SI (λk : set ⇒ pickY k) j HjSI).
We prove the intermediate claim Hfarx: ¬ (Rlt (apply_fun d (x,pickY j)) (eps_ n)).
An exact proof term for the current goal is (HfarS (pickY j) HjyS).
rewrite the current goal using HpiEq (from left to right).
An exact proof term for the current goal is Hfarx.
We prove the intermediate claim HiFI: i ∈ Fsel I Sel.
We prove the intermediate claim HdefFI: Fsel I Sel = {i0 ∈ I|∀k : set, k ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY k)) (eps_ n))}.
Use reflexivity.
rewrite the current goal using HdefFI (from left to right).
An exact proof term for the current goal is (SepI I (λi0 : set ⇒ ∀k : set, k ∈ Sel i0 → ¬ (Rlt (apply_fun d (pickY i0,pickY k)) (eps_ n))) i HiI HfarSel).
We prove the intermediate claim HiSI: i ∈ SI.
We prove the intermediate claim HiSelI: i ∈ Sel I.
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 HiSelI.
We prove the intermediate claim HxS: pickY i ∈ S.
An exact proof term for the current goal is (ReplI SI (λk : set ⇒ pickY k) i HiSI).
rewrite the current goal using HpiEq (from right to left).
An exact proof term for the current goal is HxS.
∎