Let x0 of type ι be given.

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

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

Assume H1: ∀ x2 . x2 ∈ x0 ⟶ equip (DirGraphOutNeighbors x0 x1 x2) u5.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H2: x6 ⊆ x0.

Assume H3: x5 ⊆ x0.

Assume H4: x6 = {x8 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))|equip (binintersect (DirGraphOutNeighbors x0 x1 x8) (DirGraphOutNeighbors x0 x1 x2)) u1}.

Assume H5: x4 = setminus (DirGraphOutNeighbors x0 x1 x2) (Sing x3).

Assume H6: ∀ x8 . x8 ∈ x6 ⟶ not (x1 x3 x8).

Assume H7: ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 : ο . (x8 = x2 ⟶ x9) ⟶ (x8 = x3 ⟶ x9) ⟶ (x8 ∈ x4 ⟶ x9) ⟶ (x8 ∈ x5 ⟶ x9) ⟶ (x8 ∈ x6 ⟶ x9) ⟶ (x8 ∈ x7 ⟶ x9) ⟶ x9.

Assume H8: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 : ο . (∀ x10 . x10 ∈ x6 ⟶ ∀ x11 . x11 ∈ x6 ⟶ (x10 = x11 ⟶ ∀ x12 : ο . x12) ⟶ x10 ∈ DirGraphOutNeighbors x0 x1 x8 ⟶ x11 ∈ DirGraphOutNeighbors x0 x1 x8 ⟶ not (x1 x10 x11) ⟶ (∀ x12 . x12 ∈ x6 ⟶ nIn x12 (SetAdjoin (UPair x8 x10) x11) ⟶ not (x1 x8 x12)) ⟶ x9) ⟶ x9.

Assume H9: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ ∀ x10 . x10 ∈ binintersect (DirGraphOutNeighbors x0 x1 x8) (DirGraphOutNeighbors x0 x1 x9) ⟶ x10 ∈ x6.

Assume H10: ∀ x8 . x8 ∈ x6 ⟶ nIn x8 x5.

Let x8 of type ι → ι be given.

Let x9 of type ι → ι be given.

Assume H11: ∀ x10 . x10 ∈ x6 ⟶ ∀ x11 . x11 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ x1 x11 x10 ⟶ x11 = x8 x10.

Assume H12: ∀ x10 . x10 ∈ x6 ⟶ x9 x10 ∈ x5.

Assume H13: ∀ x10 . x10 ∈ x6 ⟶ x1 x10 (x9 x10).

Assume H14: ∀ x10 . x10 ∈ x5 ⟶ ∃ x11 . and (x11 ∈ x6) (x9 x11 = x10).

Let x10 of type ι be given.

Assume H15: x10 ∈ x6.

Apply dneg with ∃ x11 . and (x11 ∈ x7) (x1 x10 x11).

Assume H16: not (∃ x11 . and (x11 ∈ x7) (x1 x10 x11)).

Apply H8 with x10, False leaving 2 subgoals.

The subproof is completed by applying H15.

Let x11 of type ι be given.

Assume H17: x11 ∈ x6.

Let x12 of type ι be given.

Assume H18: x12 ∈ x6.

Assume H19: ....

...

■

Proofgold Proof