Let x0 of type ι be given.

Assume H0: ordinal x0.

Let x1 of type ι → ο be given.

Claim L1: SNo_ x0 (PSNo x0 x1)

Apply SNo_PSNo with x0, x1.

The subproof is completed by applying H0.

Claim L2: SNo (PSNo x0 x1)

Let x2 of type ο be given.

Assume H2: ∀ x3 . and (ordinal x3) (SNo_ x3 (PSNo x0 x1)) ⟶ x2.

Apply H2 with x0.

Apply andI with ordinal x0, SNo_ x0 (PSNo x0 x1) leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying L1.

Apply SNoLev_prop with PSNo x0 x1, SNoLev (PSNo x0 x1) = x0 leaving 2 subgoals.

The subproof is completed by applying L2.

Assume H3: ordinal (SNoLev (PSNo x0 x1)).

Assume H4: SNo_ (SNoLev (PSNo x0 x1)) (PSNo x0 x1).

Apply SNoLev_uniq with PSNo x0 x1, SNoLev (PSNo x0 x1), x0 leaving 4 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H0.

The subproof is completed by applying H4.

The subproof is completed by applying L1.

■

Proofgold Proof