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.

Let x3 of type ι → ο be given.

Let x4 of type ι → ο be given.

Assume H2: PNo_least_rep x0 x1 x2 x3.

Assume H3: PNo_strict_imv x0 x1 x2 x4.

Apply H1 with ∀ x5 . x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5).

Assume H4: TransSet x2.

Assume H5: ∀ x5 . x5 ∈ x2 ⟶ TransSet x5.

Apply H2 with ∀ x5 . x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5).

Assume H6: and (ordinal x2) (PNo_strict_imv x0 x1 x2 x3).

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

Assume H7: ordinal x2.

Assume H8: PNo_strict_imv x0 x1 x2 x3.

Assume H9: ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 : ι → ο . not (PNo_strict_imv x0 x1 x5 x6).

Apply H8 with ∀ x5 . x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5).

Assume H10: PNo_strict_upperbd x0 x2 x3.

Assume H11: PNo_strict_lowerbd x1 x2 x3.

Apply H3 with ∀ x5 . x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5).

Assume H12: PNo_strict_upperbd x0 x2 x4.

Assume H13: PNo_strict_lowerbd x1 x2 x4.

Claim L14: ∀ x5 . ordinal x5 ⟶ x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5)

Apply ordinal_ind with λ x5 . x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5).

Let x5 of type ι be given.

Assume H14: ordinal x5.

Assume H15: ∀ x6 . x6 ∈ x5 ⟶ x6 ∈ x2 ⟶ iff (x3 x6) (x4 x6).

Assume H16: x5 ∈ x2.

Claim L17: ...

...

Apply iffI with x3 x5, x4 x5 leaving 2 subgoals.

Assume H18: x3 x5.

Apply dneg with x4 x5.

Assume H19: not (x4 x5).

Claim L20: PNoLt x5 x4 x2 x3

Apply PNoLtI2 with x5, x2, x4, x3 leaving 3 subgoals.

The subproof is completed by applying H16.

Apply PNoEq_sym_ with x5, x3, x4.

The subproof is completed by applying L17.

The subproof is completed by applying H18.

Claim L21: PNoLt x2 x4 x5 x4

Apply PNoLtI3 with x2, x5, x4, x4 leaving 3 subgoals.

The subproof is completed by applying H16.

The subproof is completed by applying PNoEq_ref_ with x5, x4.

The subproof is completed by applying H19.

Apply H9 with x5, x4 leaving 2 subgoals.

The subproof is completed by applying H16.

Apply andI with PNo_strict_upperbd x0 x5 x4, PNo_strict_lowerbd x1 x5 x4 leaving 2 subgoals.

Let x6 of type ι be given.

Assume H22: ordinal x6.

Let x7 of type ι → ο be given.

Assume H23: x0 x6 x7.

Apply PNoLt_tra with x6, x2, x5, x7, x4, x4 leaving 5 subgoals.

The subproof is completed by applying H22.

The subproof is completed by applying H1.

The subproof is completed by applying H14.

Apply H12 with x6, x7 leaving 2 subgoals.

The subproof is completed by applying H22.

The subproof is completed by applying H23.

The subproof is completed by applying L21.

Let x6 of type ι be given.

Assume H22: ordinal x6.

Let x7 of type ι → ο be given.

Assume H23: x1 x6 x7.

Apply PNoLt_tra with x5, x2, x6, x4, x3, x7 leaving 5 subgoals.

The subproof is completed by applying H14.

The subproof is completed by applying H1.

The subproof is completed by applying H22.

The subproof is completed by applying L20.

Apply H11 with x6, x7 leaving 2 subgoals.

The subproof is completed by applying H22.

The subproof is completed by applying H23.

...

Let x5 of type ι be given.

Assume H15: x5 ∈ x2.

Apply L14 with x5 leaving 2 subgoals.

Apply ordinal_Hered with x2, x5 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H15.

■

Proofgold Proof