Let X, W, I, idx and pickW be given.
Assume HIord: ordinal I.
Assume HWcovers: covers X W.
Assume HpointFin: ∀x : set, x ∈ X → ∃S : set, finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → x ∈ A → A ∈ S.
Assume HidxI: ∀w : set, w ∈ W → idx w ∈ I.
Assume HpickW: ∀i : set, i ∈ I → pickW i ∈ W ∧ idx (pickW i) = i.
Assume HpickW_idx: ∀w : set, w ∈ W → pickW (idx w) = w.
Let x be given.
Assume HxX: x ∈ X.
Apply (HpointFin x HxX) to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → x ∈ A → A ∈ S.
We prove the intermediate claim HS12: finite S ∧ S ⊆ W.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ W) (∀A : set, A ∈ W → x ∈ A → A ∈ S) HS).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ W) HS12).
We prove the intermediate claim HSsubW: S ⊆ W.
An exact proof term for the current goal is (andER (finite S) (S ⊆ W) HS12).
We prove the intermediate claim HScover: ∀A : set, A ∈ W → x ∈ A → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ W) (∀A : set, A ∈ W → x ∈ A → A ∈ S) HS).
Apply (HWcovers x HxX) to the current goal.
Let w0 be given.
Assume Hw0: w0 ∈ W ∧ x ∈ w0.
We prove the intermediate claim Hw0W: w0 ∈ W.
An exact proof term for the current goal is (andEL (w0 ∈ W) (x ∈ w0) Hw0).
We prove the intermediate claim Hxw0: x ∈ w0.
An exact proof term for the current goal is (andER (w0 ∈ W) (x ∈ w0) Hw0).
We prove the intermediate claim Hw0S: w0 ∈ S.
An exact proof term for the current goal is (HScover w0 Hw0W Hxw0).
Set Sx to be the term {w ∈ S|x ∈ w}.
We prove the intermediate claim Hw0Sx: w0 ∈ Sx.
An exact proof term for the current goal is (SepI S (λw : set ⇒ x ∈ w) w0 Hw0S Hxw0).
We prove the intermediate claim HSxsubS: Sx ⊆ S.
Let w be given.
Assume Hw: w ∈ Sx.
An exact proof term for the current goal is (SepE1 S (λw0 : set ⇒ x ∈ w0) w Hw).
We prove the intermediate claim HSxfin: finite Sx.
An exact proof term for the current goal is (Subq_finite S HSfin Sx HSxsubS).
We prove the intermediate claim HSxne: Sx ≠ Empty.
Assume HSx0: Sx = Empty.
We prove the intermediate claim Hcontra: w0 ∈ Empty.
rewrite the current goal using HSx0 (from right to left).
An exact proof term for the current goal is Hw0Sx.
An exact proof term for the current goal is (EmptyE w0 Hcontra).
Set Ix to be the term {idx w|w ∈ Sx}.
We prove the intermediate claim HIxfin: finite Ix.
An exact proof term for the current goal is (Repl_finite idx Sx HSxfin).
We prove the intermediate claim HIxsubI: Ix ⊆ I.
Let i be given.
Assume Hi: i ∈ Ix.
Apply (ReplE_impred Sx (λw : set ⇒ idx w) i Hi (i ∈ I)) to the current goal.
Let w be given.
Assume Hw: w ∈ Sx.
Assume Heq: i = idx w.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HwS: w ∈ S.
An exact proof term for the current goal is (SepE1 S (λw0 : set ⇒ x ∈ w0) w Hw).
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (HSsubW w HwS).
An exact proof term for the current goal is (HidxI w HwW).
We prove the intermediate claim HIxne: Ix ≠ Empty.
Assume HIx0: Ix = Empty.
We prove the intermediate claim Hcontra: idx w0 ∈ Empty.
rewrite the current goal using HIx0 (from right to left).
An exact proof term for the current goal is (ReplI Sx (λw : set ⇒ idx w) w0 Hw0Sx).
An exact proof term for the current goal is (EmptyE (idx w0) Hcontra).
Apply (finite_nonempty_subset_of_ordinal_has_max I Ix HIord HIxfin HIxsubI HIxne) to the current goal.
Let imax be given.
Assume Himax: imax ∈ Ix ∧ ∀i : set, i ∈ Ix → i ⊆ imax.
We prove the intermediate claim HimaxIx: imax ∈ Ix.
An exact proof term for the current goal is (andEL (imax ∈ Ix) (∀i : set, i ∈ Ix → i ⊆ imax) Himax).
We prove the intermediate claim HmaxSub: ∀i : set, i ∈ Ix → i ⊆ imax.
An exact proof term for the current goal is (andER (imax ∈ Ix) (∀i : set, i ∈ Ix → i ⊆ imax) Himax).
Apply (ReplE Sx (λw : set ⇒ idx w) imax HimaxIx) to the current goal.
Let wmax be given.
Assume Hwmax: wmax ∈ Sx ∧ imax = idx wmax.
We prove the intermediate claim HwmaxSx: wmax ∈ Sx.
An exact proof term for the current goal is (andEL (wmax ∈ Sx) (imax = idx wmax) Hwmax).
We prove the intermediate claim HimaxEq: imax = idx wmax.
An exact proof term for the current goal is (andER (wmax ∈ Sx) (imax = idx wmax) Hwmax).
We prove the intermediate claim HwmaxS: wmax ∈ S.
An exact proof term for the current goal is (SepE1 S (λw0 : set ⇒ x ∈ w0) wmax HwmaxSx).
We prove the intermediate claim Hxwmax: x ∈ wmax.
An exact proof term for the current goal is (SepE2 S (λw0 : set ⇒ x ∈ w0) wmax HwmaxSx).
We prove the intermediate claim HwmaxW: wmax ∈ W.
An exact proof term for the current goal is (HSsubW wmax HwmaxS).
We prove the intermediate claim HpickWimax: pickW imax = wmax.
rewrite the current goal using HimaxEq (from left to right).
An exact proof term for the current goal is (HpickW_idx wmax HwmaxW).
We use imax 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 (HIxsubI imax HimaxIx).
rewrite the current goal using HpickWimax (from left to right).
An exact proof term for the current goal is Hxwmax.
Let j be given.
Assume HjI: j ∈ I.
Assume Himaxj: imax ∈ j.
We will prove x ∉ pickW j.
Assume HxWj: x ∈ pickW j.
We prove the intermediate claim HpjW: pickW j ∈ W.
An exact proof term for the current goal is (andEL (pickW j ∈ W) (idx (pickW j) = j) (HpickW j HjI)).
We prove the intermediate claim HpjS: pickW j ∈ S.
An exact proof term for the current goal is (HScover (pickW j) HpjW HxWj).
We prove the intermediate claim HpjSx: pickW j ∈ Sx.
An exact proof term for the current goal is (SepI S (λw : set ⇒ x ∈ w) (pickW j) HpjS HxWj).
We prove the intermediate claim Hidxpj: idx (pickW j) = j.
An exact proof term for the current goal is (andER (pickW j ∈ W) (idx (pickW j) = j) (HpickW j HjI)).
We prove the intermediate claim HidxIn: idx (pickW j) ∈ Ix.
An exact proof term for the current goal is (ReplI Sx (λw : set ⇒ idx w) (pickW j) HpjSx).
We prove the intermediate claim HjIx: j ∈ Ix.
rewrite the current goal using Hidxpj (from right to left).
An exact proof term for the current goal is HidxIn.
We prove the intermediate claim HjSubImax: j ⊆ imax.
An exact proof term for the current goal is (HmaxSub j HjIx).
We prove the intermediate claim HimaxIn: imax ∈ imax.
An exact proof term for the current goal is (HjSubImax imax Himaxj).
An exact proof term for the current goal is (In_no2cycle imax imax HimaxIn HimaxIn).
∎