Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha HaL HaR.
We prove the intermediate claim L1: ∃beta, ordinal beta ∧ (∃p : set → prop, PNo_strict_imv L R beta p) ∧ ∀gamma ∈ beta, ¬ (∃p : set → prop, PNo_strict_imv L R gamma p).
Apply least_ordinal_ex (λbeta ⇒ ∃p : set → prop, PNo_strict_imv L R beta p) to the current goal.
We will prove ∃beta, ordinal beta ∧ ∃p : set → prop, PNo_strict_imv L R beta p.
Apply PNo_lenbdd_strict_imv_ex L R HLR alpha Ha HaL HaR to the current goal.
Let beta be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: beta ∈ ordsucc alpha.
Assume H1.
Apply H1 to the current goal.
Let p be given.
Assume Hp: PNo_strict_imv L R beta p.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa beta 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 beta be given.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal beta.
Assume H2: ∃p : set → prop, PNo_strict_imv L R beta p.
Assume H3: ∀gamma ∈ beta, ¬ ∃p : set → prop, PNo_strict_imv L R gamma p.
Apply H2 to the current goal.
Let p be given.
Assume Hp: PNo_strict_imv L R beta p.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
We use (λx ⇒ x ∈ beta ∧ p x) to witness the existential quantifier.
We will prove PNo_least_rep L R beta (λx ⇒ x ∈ beta ∧ p x) ∧ ∀x, x ∉ beta → ¬ (x ∈ beta ∧ p x).
Apply andI to the current goal.
We will prove ordinal beta ∧ PNo_strict_imv L R beta (λx ⇒ x ∈ beta ∧ p x) ∧ ∀gamma ∈ beta, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q.
Apply and3I to the current goal.
An exact proof term for the current goal is H1.
Apply PNoEq_strict_imv L R beta H1 p (λx ⇒ x ∈ beta ∧ p x) to the current goal.
We will prove PNoEq_ beta p (λx ⇒ x ∈ beta ∧ p x).
Let x be given.
Assume Hx: x ∈ beta.
We will prove p x ↔ x ∈ beta ∧ 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 gamma be given.
Assume Hc: gamma ∈ beta.
Let q be given.
Assume H4: PNo_strict_imv L R gamma q.
We will prove False.
Apply H3 gamma Hc to the current goal.
We will prove ∃p : set → prop, PNo_strict_imv L R gamma p.
We use q to witness the existential quantifier.
We will prove PNo_strict_imv L R gamma q.
An exact proof term for the current goal is H4.
We will prove ∀x, x ∉ beta → ¬ (x ∈ beta ∧ 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 beta q.
Assume Hr: PNo_least_rep2 L R beta 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 ∈ beta) to the current goal.
Assume H4: x ∈ beta.
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 beta r.
Assume _.
An exact proof term for the current goal is PNo_strict_imv_pred_eq L R HLR beta H1 q r Hq1 Hr1a x H4.
Assume H4: x ∉ beta.
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.
∎