Let x0 of type ι → (ι → ο) → ο be given.

Let x1 of type ι → (ι → ο) → ο be given.

Assume H0: PNoLt_pwise x0 x1.

Let x2 of type ι be given.

Assume H1: ordinal x2.

Assume H2: PNo_lenbdd x2 x0.

Assume H3: PNo_lenbdd x2 x1.

Apply PNo_rel_imv_bdd_ex with x0, x1, x2, ∃ x3 . and (x3 ∈ ordsucc x2) (∃ x4 : ι → ο . PNo_strict_imv x0 x1 x3 x4) 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.

Assume H4: (λ x4 . and (x4 ∈ ordsucc x2) (∃ x5 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x5)) x3.

Apply H4 with ∃ x4 . and (x4 ∈ ordsucc x2) (∃ x5 : ι → ο . PNo_strict_imv x0 x1 x4 x5).

Assume H5: x3 ∈ ordsucc x2.

Assume H6: ∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4.

Apply H6 with ∃ x4 . and (x4 ∈ ordsucc x2) (∃ x5 : ι → ο . PNo_strict_imv x0 x1 x4 x5).

Let x4 of type ι → ο be given.

Claim L8: ordinal (ordsucc x2)

Apply ordinal_ordsucc with x2.

The subproof is completed by applying H1.

Claim L9: ordinal x3

Apply ordinal_Hered with ordsucc x2, x3 leaving 2 subgoals.

The subproof is completed by applying L8.

The subproof is completed by applying H5.

Let x5 of type ο be given.

Assume H10: ∀ x6 . and (x6 ∈ ordsucc x2) (∃ x7 : ι → ο . PNo_strict_imv x0 x1 x6 x7) ⟶ x5.

Apply H10 with x3.

Apply andI with x3 ∈ ordsucc x2, ∃ x6 : ι → ο . PNo_strict_imv x0 x1 x3 x6 leaving 2 subgoals.

The subproof is completed by applying H5.

Let x6 of type ο be given.

Assume H11: ∀ x7 : ι → ο . PNo_strict_imv x0 x1 x3 x7 ⟶ x6.

Apply H11 with x4.

Apply PNo_rel_split_imv_imp_strict_imv with x0, x1, x3, x4 leaving 2 subgoals.

The subproof is completed by applying L9.

The subproof is completed by applying H7.

■

Proofgold Proof