Let I and S be given.
Assume HIord: ordinal I.
Assume HSfin: finite S.
Assume HSsubI: S ⊆ I.
Assume HSne: S ≠ Empty.
We will prove ∃m : set, m ∈ S ∧ ∀s : set, s ∈ S → s ⊆ m.
Set p to be the term (λX : set ⇒ X ⊆ I → (X = Empty ∨ ∃m : set, m ∈ X ∧ ∀s : set, s ∈ X → s ⊆ m)).
We prove the intermediate claim Hp0: p Empty.
Assume H0subI.
Apply orIL to the current goal.
Use reflexivity.
We prove the intermediate claim Hpstep: ∀X y : set, finite X → y ∉ X → p X → p (X ∪ {y}).
Let X and y be given.
Assume HXfin: finite X.
Assume HyX: y ∉ X.
Assume HpX: p X.
Assume HXYsubI: X ∪ {y} ⊆ I.
We will prove (X ∪ {y}) = Empty ∨ ∃m : set, m ∈ X ∪ {y} ∧ ∀s : set, s ∈ X ∪ {y} → s ⊆ m.
We prove the intermediate claim HXsubI: X ⊆ I.
Let z be given.
Assume HzX: z ∈ X.
An exact proof term for the current goal is (HXYsubI z (binunionI1 X {y} z HzX)).
We prove the intermediate claim HyI: y ∈ I.
An exact proof term for the current goal is (HXYsubI y (binunionI2 X {y} y (SingI y))).
Apply (HpX HXsubI) to the current goal.
Assume HX0: X = Empty.
Apply orIR to the current goal.
We use y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI2 X {y} y (SingI y)).
Let s be given.
Assume HsXY: s ∈ X ∪ {y}.
Apply (binunionE X {y} s HsXY) to the current goal.
Assume HsX: s ∈ X.
Apply FalseE to the current goal.
We prove the intermediate claim Hs0: s ∈ Empty.
rewrite the current goal using HX0 (from right to left).
An exact proof term for the current goal is HsX.
An exact proof term for the current goal is (EmptyE s Hs0).
Assume HsY: s ∈ {y}.
We prove the intermediate claim Hseq: s = y.
An exact proof term for the current goal is (SingE y s HsY).
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (Subq_ref y).
Assume Hexm: ∃m : set, m ∈ X ∧ ∀s : set, s ∈ X → s ⊆ m.
Apply orIR to the current goal.
Apply Hexm to the current goal.
Let m be given.
Assume Hm: m ∈ X ∧ ∀s : set, s ∈ X → s ⊆ m.
We prove the intermediate claim HmX: m ∈ X.
An exact proof term for the current goal is (andEL (m ∈ X) (∀s : set, s ∈ X → s ⊆ m) Hm).
We prove the intermediate claim HmMaxX: ∀s : set, s ∈ X → s ⊆ m.
An exact proof term for the current goal is (andER (m ∈ X) (∀s : set, s ∈ X → s ⊆ m) Hm).
We prove the intermediate claim HmI: m ∈ I.
An exact proof term for the current goal is (HXsubI m HmX).
We prove the intermediate claim HmOrd: ordinal m.
An exact proof term for the current goal is (ordinal_Hered I HIord m HmI).
We prove the intermediate claim HyOrd: ordinal y.
An exact proof term for the current goal is (ordinal_Hered I HIord y HyI).
Apply (ordinal_trichotomy_or_impred y m HyOrd HmOrd (∃mm : set, mm ∈ X ∪ {y} ∧ ∀s : set, s ∈ X ∪ {y} → s ⊆ mm)) to the current goal.
Assume Hym: y ∈ m.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 X {y} m HmX).
Let s be given.
Assume HsXY: s ∈ X ∪ {y}.
Apply (binunionE X {y} s HsXY) to the current goal.
Assume HsX: s ∈ X.
An exact proof term for the current goal is (HmMaxX s HsX).
Assume HsY: s ∈ {y}.
We prove the intermediate claim Hseq: s = y.
An exact proof term for the current goal is (SingE y s HsY).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim HmTrans: TransSet m.
An exact proof term for the current goal is (ordinal_TransSet m HmOrd).
An exact proof term for the current goal is (HmTrans y Hym).
Assume HyEq: y = m.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 X {y} m HmX).
Let s be given.
Assume HsXY: s ∈ X ∪ {y}.
Apply (binunionE X {y} s HsXY) to the current goal.
Assume HsX: s ∈ X.
An exact proof term for the current goal is (HmMaxX s HsX).
Assume HsY: s ∈ {y}.
We prove the intermediate claim Hseq: s = y.
An exact proof term for the current goal is (SingE y s HsY).
rewrite the current goal using Hseq (from left to right).
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is (Subq_ref m).
Assume Hmy: m ∈ y.
We use y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI2 X {y} y (SingI y)).
Let s be given.
Assume HsXY: s ∈ X ∪ {y}.
Apply (binunionE X {y} s HsXY) to the current goal.
Assume HsX: s ∈ X.
We prove the intermediate claim Hsm: s ⊆ m.
An exact proof term for the current goal is (HmMaxX s HsX).
We prove the intermediate claim HyTrans: TransSet y.
An exact proof term for the current goal is (ordinal_TransSet y HyOrd).
We prove the intermediate claim Hmsuby: m ⊆ y.
An exact proof term for the current goal is (HyTrans m Hmy).
An exact proof term for the current goal is (Subq_tra s m y Hsm Hmsuby).
Assume HsY: s ∈ {y}.
We prove the intermediate claim Hseq: s = y.
An exact proof term for the current goal is (SingE y s HsY).
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (Subq_ref y).
We prove the intermediate claim HpS: p S.
An exact proof term for the current goal is (finite_ind p Hp0 Hpstep S HSfin).
Apply (HpS HSsubI) to the current goal.
Assume HS0: S = Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HSne HS0).
Assume Hexm: ∃m : set, m ∈ S ∧ ∀s : set, s ∈ S → s ⊆ m.
An exact proof term for the current goal is Hexm.
∎