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.

Claim L4: ∃ x3 . and (and (ordinal x3) (∃ x4 : ι → ο . PNo_strict_imv x0 x1 x3 x4)) (∀ x4 . x4 ∈ x3 ⟶ not (∃ x5 : ι → ο . PNo_strict_imv x0 x1 x4 x5))

Apply least_ordinal_ex with λ x3 . ∃ x4 : ι → ο . PNo_strict_imv x0 x1 x3 x4.

Apply PNo_lenbdd_strict_imv_ex with x0, x1, x2, ∃ x3 . and (ordinal x3) (∃ 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_strict_imv x0 x1 x4 x5)) x3.

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

Assume H5: x3 ∈ ordsucc x2.

Assume H6: ∃ x4 : ι → ο . PNo_strict_imv ... ... ... ....

...

Apply L4 with ∃ x3 . ∃ x4 : ι → ο . PNo_least_rep x0 x1 x3 x4.

Let x3 of type ι be given.

Assume H5: (λ x4 . and (and (ordinal x4) (∃ x5 : ι → ο . PNo_strict_imv x0 x1 x4 x5)) (∀ x5 . x5 ∈ x4 ⟶ not (∃ x6 : ι → ο . PNo_strict_imv x0 x1 x5 x6))) x3.

Apply H5 with ∃ x4 . ∃ x5 : ι → ο . PNo_least_rep x0 x1 x4 x5.

Assume H6: and (ordinal x3) (∃ x4 : ι → ο . PNo_strict_imv x0 x1 x3 x4).

Apply H6 with (∀ x4 . x4 ∈ x3 ⟶ not (∃ x5 : ι → ο . PNo_strict_imv x0 x1 x4 x5)) ⟶ ∃ x4 . ∃ x5 : ι → ο . PNo_least_rep x0 x1 x4 x5.

Assume H7: ordinal x3.

Assume H8: ∃ x4 : ι → ο . PNo_strict_imv x0 x1 x3 x4.

Assume H9: ∀ x4 . x4 ∈ x3 ⟶ not (∃ x5 : ι → ο . PNo_strict_imv x0 x1 x4 x5).

Apply H8 with ∃ x4 . ∃ x5 : ι → ο . PNo_least_rep x0 x1 x4 x5.

Let x4 of type ι → ο be given.

Assume H10: PNo_strict_imv x0 x1 x3 x4.

Let x5 of type ο be given.

Assume H11: ∀ x6 . (∃ x7 : ι → ο . PNo_least_rep x0 x1 x6 x7) ⟶ x5.

Apply H11 with x3.

Let x6 of type ο be given.

Assume H12: ∀ x7 : ι → ο . PNo_least_rep x0 x1 x3 x7 ⟶ x6.

Apply H12 with x4.

Apply and3I with ordinal x3, PNo_strict_imv x0 x1 x3 x4, ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 : ι → ο . not (PNo_strict_imv x0 x1 x7 x8) leaving 3 subgoals.

The subproof is completed by applying H7.

The subproof is completed by applying H10.

Let x7 of type ι be given.

Assume H13: x7 ∈ x3.

Let x8 of type ι → ο be given.

Assume H14: PNo_strict_imv x0 x1 x7 x8.

Apply H9 with x7 leaving 2 subgoals.

The subproof is completed by applying H13.

Let x9 of type ο be given.

Assume H15: ∀ x10 : ι → ο . PNo_strict_imv x0 x1 x7 x10 ⟶ x9.

Apply H15 with x8.

The subproof is completed by applying H14.

■

Proofgold Proof