Let x0 of type ι be given.

Assume H0: x0 ∈ setexp (SNoS_ omega) omega.

Let x1 of type ι be given.

Assume H1: x1 ∈ setexp (SNoS_ omega) omega.

Assume H2: ∀ x2 . x2 ∈ omega ⟶ ∀ x3 . x3 ∈ omega ⟶ SNoLt (ap x0 x2) (ap x1 x3).

Let x2 of type ο be given.

Assume H3: SNoCutP {ap x0 x3|x3 ∈ omega} {ap x1 x3|x3 ∈ omega} ⟶ SNo (SNoCut {ap x0 x3|x3 ∈ omega} {ap x1 x3|x3 ∈ omega}) ⟶ SNoLev (SNoCut {ap x0 x3|x3 ∈ omega} {ap x1 x3|x3 ∈ omega}) ∈ ordsucc omega ⟶ SNoCut {ap x0 x3|x3 ∈ omega} {ap x1 x3|x3 ∈ omega} ∈ SNoS_ (ordsucc omega) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (ap x0 x3) (SNoCut {ap x0 x4|x4 ∈ omega} {ap x1 x4|x4 ∈ omega})) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (SNoCut {ap x0 x4|x4 ∈ omega} {ap x1 x4|x4 ∈ omega}) (ap x1 x3)) ⟶ x2.

Claim L4: ...

...

Apply SNoCutP_SNoCut_impred with {ap x0 x3|x3 ∈ omega}, {ap x1 x3|x3 ∈ omega}, x2 leaving 2 subgoals.

The subproof is completed by applying L4.

Assume H5: SNo (SNoCut {ap x0 x3|x3 ∈ omega} {ap x1 x3|x3 ∈ omega}).

Assume H6: SNoLev (SNoCut {ap x0 x3|x3 ∈ omega} {ap x1 x3|x3 ∈ omega}) ∈ ordsucc (binunion (famunion {ap x0 x3|x3 ∈ omega} (λ x3 . ordsucc (SNoLev x3))) (famunion {ap x1 x3|x3 ∈ omega} (λ x3 . ordsucc (SNoLev x3)))).

Assume H7: ∀ x3 . x3 ∈ {ap x0 x4|x4 ∈ omega} ⟶ SNoLt x3 (SNoCut {ap x0 x4|x4 ∈ omega} {ap x1 x4|x4 ∈ omega}).

Assume H8: ∀ x3 . x3 ∈ {ap x1 x4|x4 ∈ omega} ⟶ SNoLt (SNoCut {ap x0 x4|x4 ∈ omega} {ap x1 x4|x4 ∈ omega}) x3.

Assume H9: ∀ x3 . ... ⟶ ... ⟶ (∀ x4 . x4 ∈ {...|x5 ∈ omega} ⟶ SNoLt x3 x4) ⟶ and (SNoLev (SNoCut {ap x0 x4|x4 ∈ omega} {ap x1 x4|x4 ∈ omega}) ⊆ SNoLev x3) (SNoEq_ (SNoLev (SNoCut {ap x0 x4|x4 ∈ omega} {ap x1 x4|x4 ∈ omega})) (SNoCut {ap x0 x4|x4 ∈ omega} {ap x1 x4|x4 ∈ omega}) x3).

...

■

Proofgold Proof