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

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

Let x2 of type ι be given.

Assume H0: ordinal x2.

Let x3 of type ι → ο be given.

Assume H1: ∀ x4 . x4 ∈ x2 ⟶ x3 x4.

Assume H2: ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x0 x4 x5 ⟶ x4 ∈ x2.

Assume H3: ∀ x4 . x4 ∈ x2 ⟶ x0 x4 x3.

Assume H4: ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . not (x1 x4 x5).

Apply andI with PNo_strict_upperbd x0 x2 x3, PNo_strict_lowerbd x1 x2 x3 leaving 2 subgoals.

Let x4 of type ι be given.

Assume H5: ordinal x4.

Let x5 of type ι → ο be given.

Assume H6: x0 x4 x5.

Claim L7: x4 ∈ x2

Apply H2 with x4, x5 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

Apply PNoLt_trichotomy_or with x2, x4, x3, x5, PNoLt x4 x5 x2 x3 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H5.

Assume H8: or (PNoLt x2 x3 x4 x5) (and (x2 = x4) (PNoEq_ x2 x3 x5)).

Apply H8 with PNoLt x4 x5 x2 x3 leaving 2 subgoals.

Assume H9: PNoLt x2 x3 x4 x5.

Apply FalseE with PNoLt x4 x5 x2 x3.

Apply PNoLtE with x2, x4, x3, x5, False leaving 4 subgoals.

The subproof is completed by applying H9.

Assume H10: PNoLt_ (binintersect x2 x4) x3 x5.

Apply PNoLt_E_ with binintersect x2 x4, x3, x5, False leaving 2 subgoals.

The subproof is completed by applying H10.

Let x6 of type ι be given.

Assume H11: x6 ∈ binintersect x2 x4.

Apply binintersectE with x2, x4, x6, PNoEq_ x6 x3 x5 ⟶ not (x3 x6) ⟶ x5 x6 ⟶ False leaving 2 subgoals.

The subproof is completed by applying H11.

Assume H12: x6 ∈ x2.

Assume H13: x6 ∈ x4.

Assume H14: PNoEq_ x6 x3 x5.

Assume H15: not (x3 x6).

Apply FalseE with x5 x6 ⟶ False.

Apply H15.

Apply H1 with x6.

The subproof is completed by applying H12.

Assume H10: x2 ∈ x4.

Apply FalseE with PNoEq_ x2 x3 x5 ⟶ x5 x2 ⟶ False.

Apply In_no2cycle with x2, x4 leaving 2 subgoals.

The subproof is completed by applying H10.

The subproof is completed by applying L7.

Assume H10: x4 ∈ x2.

Assume H11: PNoEq_ x4 x3 x5.

Assume H12: not (x3 x4).

Apply H12.

Apply H1 with x4.

The subproof is completed by applying L7.

Assume H9: and (x2 = x4) (PNoEq_ x2 x3 x5).

Apply H9 with PNoLt x4 x5 x2 x3.

Assume H10: x2 = x4.

Apply FalseE with PNoEq_ x2 x3 x5 ⟶ PNoLt x4 x5 x2 x3.

Apply In_irref with x2.

Apply H10 with λ x6 x7 . x7 ∈ x2.

The subproof is completed by applying L7.

Assume H8: PNoLt x4 x5 x2 x3.

The subproof is completed by applying H8.

Let x4 of type ι be given.

Assume H5: ordinal x4.

Let x5 of type ι → ο be given.

Assume H6: x1 x4 x5.

Apply FalseE with PNoLt x2 x3 x4 x5.

Apply H4 with x4, x5 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

■

Proofgold Proof