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

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι → ο be given.

Let x4 of type ι → ο be given.

Assume H0: ordinal x1.

Assume H1: ordinal x2.

Assume H2: 8356a.. x0 x1 x3.

Assume H3: 35b9b.. x2 x4 x1 x3.

Apply H2 with 8356a.. x0 x2 x4.

Let x5 of type ι be given.

Assume H4: (λ x6 . and (ordinal x6) (∃ x7 : ι → ο . and (x0 x6 x7) (35b9b.. x1 x3 x6 x7))) x5.

Apply H4 with 8356a.. x0 x2 x4.

Assume H5: ordinal x5.

Assume H6: ∃ x6 : ι → ο . and (x0 x5 x6) (35b9b.. x1 x3 x5 x6).

Apply H6 with 8356a.. x0 x2 x4.

Let x6 of type ι → ο be given.

Assume H7: (λ x7 : ι → ο . and (x0 x5 x7) (35b9b.. x1 x3 x5 x7)) x6.

Apply H7 with 8356a.. x0 x2 x4.

Assume H8: x0 x5 x6.

Assume H9: 35b9b.. x1 x3 x5 x6.

Let x7 of type ο be given.

Assume H10: ∀ x8 . and (ordinal x8) (∃ x9 : ι → ο . and (x0 x8 x9) (35b9b.. x2 x4 x8 x9)) ⟶ x7.

Apply H10 with x5.

Apply andI with ordinal x5, ∃ x8 : ι → ο . and (x0 x5 x8) (35b9b.. x2 x4 x5 x8) leaving 2 subgoals.

The subproof is completed by applying H5.

Let x8 of type ο be given.

Assume H11: ∀ x9 : ι → ο . and (x0 x5 x9) (35b9b.. x2 x4 x5 x9) ⟶ x8.

Apply H11 with x6.

Apply andI with x0 x5 x6, 35b9b.. x2 x4 x5 x6 leaving 2 subgoals.

The subproof is completed by applying H8.

Apply unknownprop_e2fba515d4f4b73abb6664acd434e29949a2b63c3796bbc956c77c7f4dcece18 with x2, x1, x5, x4, x3, x6 leaving 5 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H0.

The subproof is completed by applying H5.

The subproof is completed by applying H3.

The subproof is completed by applying H9.

■

Proofgold Proof