Let x0 of type ι be given.

Apply unknownprop_7e7a3c7a04dac475d679ef0eb25eb83b9a217d071452ad37861b7c785c606e42 with λ x1 x2 : ι → ο . x2 x0 ⟶ ∀ x3 : ο . (∀ x4 . ordinal x4 ⟶ SNo_ x4 x0 ⟶ x3) ⟶ x3.

Assume H0: (λ x1 . ∃ x2 . and (ordinal x2) (SNo_ x2 x1)) x0.

Let x1 of type ο be given.

Assume H1: ∀ x2 . ordinal x2 ⟶ SNo_ x2 x0 ⟶ x1.

Apply H0 with x1.

Let x2 of type ι be given.

Assume H2: (λ x3 . and (ordinal x3) (SNo_ x3 x0)) x2.

Apply andE with ordinal x2, SNo_ x2 x0, x1 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H1 with x2.

■

Proofgold Proof