Let x0 of type ι → ι → ι → ο be given.

Assume H0: ∀ x1 . ordinal x1 ⟶ ∀ x2 . ordinal x2 ⟶ ∀ x3 . ordinal x3 ⟶ ∀ x4 . x4 ∈ SNoS_ x1 ⟶ ∀ x5 . x5 ∈ SNoS_ x2 ⟶ ∀ x6 . x6 ∈ SNoS_ x3 ⟶ x0 x4 x5 x6.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H1: SNo x1.

Assume H2: SNo x2.

Assume H3: SNo x3.

Claim L4: ordinal (SNoLev x1)

Apply SNoLev_ordinal with x1.

The subproof is completed by applying H1.

Claim L5: ordinal (ordsucc (SNoLev x1))

Apply ordinal_ordsucc with SNoLev x1.

The subproof is completed by applying L4.

Claim L6: x1 ∈ SNoS_ (ordsucc (SNoLev x1))

Apply SNoS_SNoLev with x1.

The subproof is completed by applying H1.

Claim L7: ordinal (SNoLev x2)

Apply SNoLev_ordinal with x2.

The subproof is completed by applying H2.

Claim L8: ordinal (ordsucc (SNoLev x2))

Apply ordinal_ordsucc with SNoLev x2.

The subproof is completed by applying L7.

Claim L9: x2 ∈ SNoS_ (ordsucc (SNoLev x2))

Apply SNoS_SNoLev with x2.

The subproof is completed by applying H2.

Claim L10: ordinal (SNoLev x3)

Apply SNoLev_ordinal with x3.

The subproof is completed by applying H3.

Claim L11: ordinal (ordsucc (SNoLev x3))

Apply ordinal_ordsucc with SNoLev x3.

The subproof is completed by applying L10.

Claim L12: x3 ∈ SNoS_ (ordsucc (SNoLev x3))

Apply SNoS_SNoLev with x3.

The subproof is completed by applying H3.

Apply H0 with ordsucc (SNoLev x1), ordsucc (SNoLev x2), ordsucc (SNoLev x3), x1, x2, x3 leaving 6 subgoals.

The subproof is completed by applying L5.

The subproof is completed by applying L8.

The subproof is completed by applying L11.

The subproof is completed by applying L6.

The subproof is completed by applying L9.

The subproof is completed by applying L12.

■

Proofgold Proof