Let x0 of type ι be given.

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

Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2.

Assume H1: 4402e.. x0 x1.

Assume H2: cf2df.. x0 x1.

Let x2 of type ι be given.

Assume H3: x2 ∈ x0.

Let x3 of type ι be given.

Assume H4: x3 ⊆ setminus x0 (Sing x2).

Assume H5: ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ x1 x4 x5 ⟶ x1 x5 x4.

Assume H6: atleastp u10 x3.

Assume H7: 4402e.. x3 x1.

Assume H8: cf2df.. x3 x1.

Let x4 of type ο be given.

Assume H9: a0244.. x0 x1 ⟶ x4.

Assume H10: ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ f1c88.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4.

Assume H11: ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 97406.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4.

Assume H12: ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 0d539.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4.

Assume H13: ∀ x5 . ... ⟶ ∀ x6 . x6 ∈ ... ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 4b1cb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4.

...

■

Proofgold Proof