Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNoCutP x0 x1.

Apply SNoCutP_SNoCut with x0, x1, SNo (SNoCut x0 x1) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: and (and (and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1) ∈ ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2)))))) (∀ x2 . x2 ∈ x0 ⟶ SNoLt x2 (SNoCut x0 x1))) (∀ x2 . x2 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x2).

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

Apply H1 with SNo (SNoCut x0 x1).

Assume H3: and (and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1) ∈ ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2)))))) (∀ x2 . x2 ∈ x0 ⟶ SNoLt x2 (SNoCut x0 x1)).

Assume H4: ∀ x2 . x2 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x2.

Apply H3 with SNo (SNoCut x0 x1).

Assume H5: and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1) ∈ ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2))))).

Assume H6: ∀ x2 . x2 ∈ x0 ⟶ SNoLt x2 (SNoCut x0 x1).

Apply H5 with SNo (SNoCut x0 x1).

Assume H7: SNo (SNoCut x0 x1).

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

The subproof is completed by applying H7.

■

Proofgold Proof