Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNoCutP x0 x1.

Let x2 of type ι be given.

Assume H1: x2 ∈ SNoL (SNoCut x0 x1).

Apply dneg with ∃ x3 . and (x3 ∈ x0) (SNoLe x2 x3).

Assume H2: not (∃ x3 . and (x3 ∈ x0) (SNoLe x2 x3)).

Apply H0 with False.

Assume H3: and (∀ x3 . x3 ∈ x0 ⟶ SNo x3) (∀ x3 . x3 ∈ x1 ⟶ SNo x3).

Apply H3 with (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 ⟶ SNoLt x3 x4) ⟶ False.

Assume H4: ∀ x3 . x3 ∈ x0 ⟶ SNo x3.

Assume H5: ∀ x3 . x3 ∈ x1 ⟶ SNo x3.

Assume H6: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 ⟶ SNoLt x3 x4.

Apply SNoCutP_SNoCut_impred with x0, x1, False leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H7: SNo (SNoCut x0 x1).

Assume H8: SNoLev (SNoCut x0 x1) ∈ ordsucc (binunion (famunion x0 (λ x3 . ordsucc (SNoLev x3))) (famunion x1 (λ x3 . ordsucc (SNoLev x3)))).

Assume H9: ∀ x3 . x3 ∈ x0 ⟶ SNoLt x3 (SNoCut x0 x1).

Assume H10: ∀ x3 . x3 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x3.

Assume H11: ∀ x3 . SNo x3 ⟶ (∀ x4 . x4 ∈ x0 ⟶ SNoLt x4 x3) ⟶ (∀ x4 . x4 ∈ x1 ⟶ SNoLt x3 x4) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x3) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x3).

Apply SNoL_E with SNoCut x0 x1, x2, False leaving 3 subgoals.

The subproof is completed by applying H7.

The subproof is completed by applying H1.

Assume H12: SNo x2.

Assume H13: SNoLev x2 ∈ SNoLev (SNoCut x0 x1).

Assume H14: SNoLt x2 (SNoCut x0 x1).

Apply In_irref with SNoLev x2.

Apply andEL with SNoLev (SNoCut x0 x1) ⊆ SNoLev x2, SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2, SNoLev x2 leaving 2 subgoals.

Apply H11 with x2 leaving 3 subgoals.

The subproof is completed by applying H12.

Let x3 of type ι be given.

Assume H15: x3 ∈ x0.

Apply SNoLtLe_or with x3, x2, SNoLt x3 x2 leaving 4 subgoals.

Apply H4 with x3.

The subproof is completed by applying H15.

The subproof is completed by applying H12.

Assume H16: SNoLt x3 x2.

The subproof is completed by applying H16.

Assume H16: SNoLe x2 x3.

Apply H2 with SNoLt x3 x2.

Let x4 of type ο be given.

Assume H17: ∀ x5 . and (x5 ∈ x0) (SNoLe x2 x5) ⟶ x4.

Apply H17 with x3.

Apply andI with x3 ∈ x0, SNoLe x2 x3 leaving 2 subgoals.

The subproof is completed by applying H15.

The subproof is completed by applying H16.

Let x3 of type ι be given.

Assume H15: x3 ∈ x1.

Apply SNoLt_tra with x2, SNoCut x0 x1, x3 leaving 5 subgoals.

The subproof is completed by applying H12.

The subproof is completed by applying H7.

Apply H5 with x3.

The subproof is completed by applying H15.

The subproof is completed by applying H14.

Apply H10 with x3.

The subproof is completed by applying H15.

The subproof is completed by applying H13.

■

Proofgold Proof