Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha HaL HaR.
Apply PNo_bd_pred L R HLR alpha Ha HaL HaR to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal (PNo_bd L R).
Assume H2: PNo_strict_imv L R (PNo_bd L R) (PNo_pred L R).
Assume H3: ∀gamma ∈ PNo_bd L R, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q.
Apply PNo_lenbdd_strict_imv_ex L R HLR alpha Ha HaL HaR to the current goal.
Let beta be given.
Assume H4.
Apply H4 to the current goal.
Assume Hb: beta ∈ ordsucc alpha.
Assume H4.
Apply H4 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.
Apply ordinal_In_Or_Subq (PNo_bd L R) (ordsucc alpha) H1 Lsa to the current goal.
Assume H4: PNo_bd L R ∈ ordsucc alpha.
An exact proof term for the current goal is H4.
Assume H4: ordsucc alpha ⊆ PNo_bd L R.
We will prove False.
We prove the intermediate claim Lb: beta ∈ PNo_bd L R.
Apply H4 to the current goal.
An exact proof term for the current goal is Hb.
Apply H3 beta Lb p to the current goal.
An exact proof term for the current goal is Hp.
∎