Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H1: x2 ⊆ x0.
Assume H2: x3 ⊆ x0.
Assume H3: x4 ⊆ x0.
Assume H4: x5 ⊆ x0.
Assume H5:
∀ x6 . x6 ∈ x2 ⟶ nIn x6 x5.
Assume H6:
∀ x6 . x6 ∈ x2 ⟶ nIn x6 x3.
Assume H7:
∀ x6 . x6 ∈ x4 ⟶ nIn x6 x2.
Assume H8:
∀ x6 . x6 ∈ x4 ⟶ nIn x6 x3.
Assume H9:
∀ x6 . x6 ∈ x4 ⟶ nIn x6 x5.
Assume H10:
∀ x6 . x6 ∈ x3 ⟶ nIn x6 x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι be given.
Assume H12: x10 ∈ x5.
Assume H16:
not (x1 x7 x10).
Assume H17:
not (x1 x9 x10).
Let x11 of type ι → ι be given.
Let x12 of type ι → ι be given.
Assume H18: ∀ x13 . x13 ∈ x4 ⟶ x11 x13 ∈ x2.
Assume H20: ∀ x13 . x13 ∈ x4 ⟶ x12 x13 ∈ x3.
Apply H11 with
λ x13 x14 . ∀ x15 . x15 ∈ x14 ⟶ x15 ∈ {x16 ∈ setminus x4 (Sing x6)|x1 (x11 x16) x10} ⟶ x15 ∈ {x16 ∈ setminus x4 (Sing x6)|x1 (x12 x16) x10} ⟶ x15 = x8.
Apply unknownprop_cb75c47bae3a116273752c6fc8e52c777498313f2b5b4ef43d3ceb63348e2717 with
x6,
x7,
x8,
x9,
λ x13 . x13 ∈ {x14 ∈ setminus x4 (Sing x6)|x1 (x11 x14) x10} ⟶ x13 ∈ {x14 ∈ setminus x4 (Sing x6)|x1 (x12 x14) x10} ⟶ x13 = x8 leaving 4 subgoals.
Assume H31:
x6 ∈ {x13 ∈ setminus x4 (Sing x6)|x1 (x11 x13) x10}.
Apply FalseE with
x6 ∈ {x13 ∈ setminus x4 (Sing x6)|x1 (x12 x13) x10} ⟶ x6 = x8.
Apply setminusE2 with
x4,
Sing x6,
x6 leaving 2 subgoals.
Apply SepE1 with
setminus ... ...,
...,
....