Let I and S be given.
Assume HordI: ordinal I.
Assume HSsubI: S ⊆ I.
Assume HSne: S ≠ Empty.
We will prove ∃m : set, m ∈ S ∧ ∀s : set, s ∈ S → m ⊆ s.
We prove the intermediate claim Hexs: ∃x : set, x ∈ S.
An exact proof term for the current goal is (nonempty_has_element S HSne).
Apply Hexs to the current goal.
Let x be given.
Assume HxS: x ∈ S.
Set p to be the term λa : set ⇒ a ∈ S.
We prove the intermediate claim Hexord: ∃a : set, ordinal a ∧ p a.
We use x to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HxI: x ∈ I.
An exact proof term for the current goal is (HSsubI x HxS).
An exact proof term for the current goal is (ordinal_Hered I HordI x HxI).
An exact proof term for the current goal is HxS.
Apply (least_ordinal_ex p Hexord) to the current goal.
Let m be given.
Assume Hm: ordinal m ∧ p m ∧ ∀beta ∈ m, ¬ p beta.
We prove the intermediate claim Hm12: ordinal m ∧ p m.
An exact proof term for the current goal is (andEL (ordinal m ∧ p m) (∀beta ∈ m, ¬ p beta) Hm).
We prove the intermediate claim Hmord: ordinal m.
An exact proof term for the current goal is (andEL (ordinal m) (p m) Hm12).
We prove the intermediate claim Hmp: p m.
An exact proof term for the current goal is (andER (ordinal m) (p m) Hm12).
We prove the intermediate claim Hmmin: ∀beta ∈ m, ¬ p beta.
An exact proof term for the current goal is (andER (ordinal m ∧ p m) (∀beta ∈ m, ¬ p beta) Hm).
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hmp.
Let s be given.
Assume HsS: s ∈ S.
We prove the intermediate claim Hsord: ordinal s.
We prove the intermediate claim HsI: s ∈ I.
An exact proof term for the current goal is (HSsubI s HsS).
An exact proof term for the current goal is (ordinal_Hered I HordI s HsI).
Apply (ordinal_trichotomy_or_impred m s Hmord Hsord (m ⊆ s)) to the current goal.
Assume Hms: m ∈ s.
We prove the intermediate claim HsTr: TransSet s.
An exact proof term for the current goal is (andEL (TransSet s) (∀beta ∈ s, TransSet beta) Hsord).
An exact proof term for the current goal is (HsTr m Hms).
Assume Hmeq: m = s.
rewrite the current goal using Hmeq (from left to right).
An exact proof term for the current goal is (Subq_ref s).
Assume Hsm: s ∈ m.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hmmin s Hsm HsS).
∎