Let L and R be given.
Assume HLR.
Let α be given.
Assume Ha HaL HaR.
We prove the intermediate claim L1: ∃β, ordinal β ∧ (∃p : set → prop, PNo_strict_imv L R β p) ∧ ∀γ ∈ β, ¬ (∃p : set → prop, PNo_strict_imv L R γ p).
Apply least_ordinal_ex (λβ ⇒ ∃p : set → prop, PNo_strict_imv L R β p) to the current goal.
We will prove ∃β, ordinal β ∧ ∃p : set → prop, PNo_strict_imv L R β p.
Apply PNo_lenbdd_strict_imv_ex L R HLR α Ha HaL HaR to the current goal.
Let β be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: β ∈ ordsucc α.
Assume H1.
Apply H1 to the current goal.
Let p be given.
Assume Hp: PNo_strict_imv L R β p.
We prove the intermediate claim Lsa: ordinal (ordsucc α).
An exact proof term for the current goal is ordinal_ordsucc α Ha.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is ordinal_Hered (ordsucc α) Lsa β Hb.
We use p to witness the existential quantifier.
An exact proof term for the current goal is Hp.
Apply L1 to the current goal.
Let β be given.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal β.
Assume H2: ∃p : set → prop, PNo_strict_imv L R β p.
Assume H3: ∀γ ∈ β, ¬ ∃p : set → prop, PNo_strict_imv L R γ p.
Apply H2 to the current goal.
Let p be given.
Assume Hp: PNo_strict_imv L R β p.
We use β to witness the existential quantifier.
Apply andI to the current goal.
We use (λx ⇒ x ∈ β ∧ p x) to witness the existential quantifier.
We will prove PNo_least_rep L R β (λx ⇒ x ∈ β ∧ p x) ∧ ∀x, x ∉ β → ¬ (x ∈ β ∧ p x).
Apply andI to the current goal.
We will prove ordinal β ∧ PNo_strict_imv L R β (λx ⇒ x ∈ β ∧ p x) ∧ ∀γ ∈ β, ∀q : set → prop, ¬ PNo_strict_imv L R γ q.
Apply and3I to the current goal.
An exact proof term for the current goal is H1.
Apply PNoEq_strict_imv L R β H1 p (λx ⇒ x ∈ β ∧ p x) to the current goal.
We will prove PNoEq_ β p (λx ⇒ x ∈ β ∧ p x).
Let x be given.
Assume Hx: x ∈ β.
We will prove p x ↔ x ∈ β ∧ p x.
Apply iffI to the current goal.
Assume H4.
Apply andI to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is H4.
Assume H4.
Apply H4 to the current goal.
Assume _ H5.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is Hp.
Let γ be given.
Assume Hc: γ ∈ β.
Let q be given.
Assume H4: PNo_strict_imv L R γ q.
We will prove False.
Apply H3 γ Hc to the current goal.
We will prove ∃p : set → prop, PNo_strict_imv L R γ p.
We use q to witness the existential quantifier.
We will prove PNo_strict_imv L R γ q.
An exact proof term for the current goal is H4.
We will prove ∀x, x ∉ β → ¬ (x ∈ β ∧ p x).
Let x be given.
Assume Hx.
Assume H4.
Apply H4 to the current goal.
Assume H5 _.
An exact proof term for the current goal is Hx H5.
Let q and r be given.
Assume Hq: PNo_least_rep2 L R β q.
Assume Hr: PNo_least_rep2 L R β r.
Apply Hq to the current goal.
Assume Hq1 Hq2.
Apply Hr to the current goal.
Assume Hr1 Hr2.
We will prove q = r.
Apply pred_ext to the current goal.
Let x be given.
Apply xm (x ∈ β) to the current goal.
Assume H4: x ∈ β.
We will prove q x ↔ r x.
Apply Hr1 to the current goal.
Assume Hr1a.
Apply Hr1a to the current goal.
Assume _.
Assume Hr1a: PNo_strict_imv L R β r.
Assume _.
An exact proof term for the current goal is PNo_strict_imv_pred_eq L R HLR β H1 q r Hq1 Hr1a x H4.
Assume H4: x ∉ β.
Apply iffI to the current goal.
Assume H5: q x.
We will prove False.
Apply Hq2 x H4 to the current goal.
An exact proof term for the current goal is H5.
Assume H5: r x.
We will prove False.
Apply Hr2 x H4 to the current goal.
An exact proof term for the current goal is H5.
∎