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

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

Assume H0: PNoLt_pwise x0 x1.

Claim L1: ...

...

Apply ordinal_ind with λ x2 . or (∃ x3 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x3) (∃ x3 . and (x3 ∈ x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4)).

Let x2 of type ι be given.

Assume H2: ordinal x2.

Apply H2 with (∀ x3 . x3 ∈ x2 ⟶ or (∃ x4 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x3 x4) (∃ x4 . and (x4 ∈ x3) (∃ x5 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x5))) ⟶ or (∃ x3 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x3) (∃ x3 . and (x3 ∈ x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4)).

Assume H3: TransSet x2.

Assume H4: ∀ x3 . x3 ∈ x2 ⟶ TransSet x3.

Assume H5: ∀ x3 . x3 ∈ x2 ⟶ or (∃ x4 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x3 x4) (∃ x4 . and (x4 ∈ x3) (∃ x5 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x5)).

Apply dneg with or (∃ x3 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x3) (∃ x3 . and (x3 ∈ x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4)).

Assume H6: not (or (∃ x3 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x3) (∃ x3 . and (x3 ∈ x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4))).

Apply not_or_and_demorgan with ∃ x3 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x3, ∃ x3 . and (x3 ∈ x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4), False leaving 2 subgoals.

The subproof is completed by applying H6.

Assume H7: not (∃ x3 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x3).

Assume H8: not (∃ x3 . and (x3 ∈ x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4)).

Claim L9: ...

...

Apply ordinal_lim_or_succ with x2, False leaving 3 subgoals.

The subproof is completed by applying H2.

Assume H10: ∀ x3 . x3 ∈ x2 ⟶ ordsucc x3 ∈ x2.

Claim L11: ...

...

Claim L12: ...

...

Apply H7.

Let x3 of type ο be given.

Assume H13: ∀ x4 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x4 ⟶ x3.

Apply H13 with λ x4 . ∀ x5 : ι → ο . PNo_rel_strict_imv x0 x1 (ordsucc x4) x5 ⟶ x5 x4.

Apply andI with PNo_rel_strict_imv x0 x1 x2 (λ x4 . ∀ x5 : ι → ο . PNo_rel_strict_imv x0 x1 (ordsucc x4) x5 ⟶ x5 x4), ∀ x4 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x4 ⟶ PNoEq_ x2 (λ x5 . ∀ x6 : ι → ο . PNo_rel_strict_imv x0 x1 (ordsucc x5) x6 ⟶ x6 x5) x4 leaving 2 subgoals.

Apply andI with PNo_rel_strict_upperbd x0 x2 (λ x4 . ∀ x5 : ι → ο . PNo_rel_strict_imv x0 x1 (ordsucc x4) x5 ⟶ x5 x4), PNo_rel_strict_lowerbd x1 x2 (λ x4 . ∀ x5 : ι → ο . PNo_rel_strict_imv x0 x1 ... ... ⟶ x5 x4) leaving 2 subgoals.

...

■

Proofgold Proof