Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Apply PNo_bd_pred with
x0,
x1,
x2,
PNo_bd x0 x1 ∈ ordsucc x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply H4 with
(∀ x3 . x3 ∈ PNo_bd x0 x1 ⟶ ∀ x4 : ι → ο . not (PNo_strict_imv x0 x1 x3 x4)) ⟶ PNo_bd x0 x1 ∈ ordsucc x2.
Apply PNo_lenbdd_strict_imv_ex with
x0,
x1,
x2,
PNo_bd x0 x1 ∈ ordsucc x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Apply H8 with
PNo_bd x0 x1 ∈ ordsucc x2.
Apply H10 with
PNo_bd x0 x1 ∈ ordsucc x2.
Let x4 of type ι → ο be given.
Apply ordinal_ordsucc with
x2.
The subproof is completed by applying H1.
Apply ordinal_In_Or_Subq with
PNo_bd x0 x1,
ordsucc x2,
PNo_bd x0 x1 ∈ ordsucc x2 leaving 4 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying L12.
The subproof is completed by applying H13.
Apply FalseE with
PNo_bd x0 x1 ∈ ordsucc x2.
Claim L14:
x3 ∈ PNo_bd x0 x1
Apply H13 with
x3.
The subproof is completed by applying H9.
Apply H7 with
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying L14.
The subproof is completed by applying H11.