Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNoCutP x0 x1.

Apply H0 with SNoCutP {minus_SNo x2|x2 ∈ x1} {minus_SNo x2|x2 ∈ x0}.

Assume H1: and (∀ x2 . x2 ∈ x0 ⟶ SNo x2) (∀ x2 . x2 ∈ x1 ⟶ SNo x2).

Apply H1 with (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3) ⟶ SNoCutP {minus_SNo x2|x2 ∈ x1} {minus_SNo x2|x2 ∈ x0}.

Assume H2: ∀ x2 . x2 ∈ x0 ⟶ SNo x2.

Assume H3: ∀ x2 . x2 ∈ x1 ⟶ SNo x2.

Assume H4: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3.

Apply and3I with ∀ x2 . x2 ∈ {minus_SNo x3|x3 ∈ x1} ⟶ SNo x2, ∀ x2 . x2 ∈ {minus_SNo x3|x3 ∈ x0} ⟶ SNo x2, ∀ x2 . x2 ∈ {minus_SNo x3|x3 ∈ x1} ⟶ ∀ x3 . x3 ∈ {minus_SNo x4|x4 ∈ x0} ⟶ SNoLt x2 x3 leaving 3 subgoals.

Let x2 of type ι be given.

Assume H5: x2 ∈ {minus_SNo x3|x3 ∈ x1}.

Apply ReplE_impred with x1, λ x3 . minus_SNo x3, x2, SNo x2 leaving 2 subgoals.

The subproof is completed by applying H5.

Let x3 of type ι be given.

Assume H6: x3 ∈ x1.

Assume H7: x2 = minus_SNo x3.

Apply H7 with λ x4 x5 . SNo x5.

Apply SNo_minus_SNo with x3.

Apply H3 with x3.

The subproof is completed by applying H6.

Let x2 of type ι be given.

Assume H5: x2 ∈ {minus_SNo x3|x3 ∈ x0}.

Apply ReplE_impred with x0, λ x3 . minus_SNo x3, x2, SNo x2 leaving 2 subgoals.

The subproof is completed by applying H5.

Let x3 of type ι be given.

Assume H6: x3 ∈ x0.

Assume H7: x2 = minus_SNo x3.

Apply H7 with λ x4 x5 . SNo x5.

Apply SNo_minus_SNo with x3.

Apply H2 with x3.

The subproof is completed by applying H6.

Let x2 of type ι be given.

Assume H5: x2 ∈ {minus_SNo x3|x3 ∈ x1}.

Let x3 of type ι be given.

Assume H6: x3 ∈ {minus_SNo x4|x4 ∈ x0}.

Apply ReplE_impred with x1, λ x4 . minus_SNo x4, x2, SNoLt x2 x3 leaving 2 subgoals.

The subproof is completed by applying H5.

Let x4 of type ι be given.

Assume H7: x4 ∈ x1.

Assume H8: x2 = minus_SNo x4.

Apply ReplE_impred with x0, λ x5 . minus_SNo x5, x3, SNoLt x2 x3 leaving 2 subgoals.

The subproof is completed by applying H6.

Let x5 of type ι be given.

Assume H9: x5 ∈ x0.

Assume H10: x3 = minus_SNo x5.

Apply H8 with λ x6 x7 . SNoLt x7 x3.

Apply H10 with λ x6 x7 . SNoLt (minus_SNo x4) x7.

Apply minus_SNo_Lt_contra with x5, x4 leaving 3 subgoals.

Apply H2 with x5.

The subproof is completed by applying H9.

Apply H3 with x4.

The subproof is completed by applying H7.

Apply H4 with x5, x4 leaving 2 subgoals.

The subproof is completed by applying H9.

The subproof is completed by applying H7.

■

Proofgold Proof