Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNoCutP x0 x1.

Apply SNoCutP_SNoCut with x0, x1, ∀ x2 . x2 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x2 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 ∀ x2 . x2 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x2.

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.

The subproof is completed by applying H4.

■

Proofgold Proof