Let L and R be given.
Assume HLR.
Let α be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume HaL HaR.
We prove the intermediate claim Lsa: ordinal (ordsucc α).
An exact proof term for the current goal is ordinal_ordsucc α Ha.
Apply PNo_rel_imv_ex L R HLR α Ha to the current goal.
Assume H2.
Apply H2 to the current goal.
Let p be given.
Assume Hp: PNo_rel_strict_uniq_imv L R α p.
Apply Hp to the current goal.
Assume Hp1: PNo_rel_strict_imv L R α p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Assume Hp2: ∀q : set → prop, PNo_rel_strict_imv L R α q → PNoEq_ α p q.
We use α to witness the existential quantifier.
Apply andI to the current goal.
We will prove α ∈ ordsucc α.
Apply ordsuccI2 to the current goal.
We use p to witness the existential quantifier.
We will prove PNo_rel_strict_split_imv L R α p.
An exact proof term for the current goal is PNo_lenbdd_strict_imv_split L R α Ha HaL HaR p Hp1.
Assume H1.
Apply H1 to the current goal.
Let β be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: β ∈ α.
Assume H1.
We use β to witness the existential quantifier.
Apply andI to the current goal.
We will prove β ∈ ordsucc α.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is H1.
∎