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 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4).

Assume H2: ∀ x2 . x2 ⊆ x0 ⟶ atleastp u6 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x1 x3 x4)).

Let x2 of type ι be given.

Assume H3: nat_p x2.

Assume H4: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x1 x3 x4) ⟶ or (equip (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x4)) x2) (equip (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x4)) (ordsucc x2)).

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H5: x3 ∈ x0.

Assume H6: x4 ∈ DirGraphOutNeighbors x0 x1 x3.

Assume H7: ∀ x5 . x5 ∈ {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) x2} ⟶ not (x1 x4 x5).

Apply unknownprop_891efbf0f888d5ec549c9ff814ca1cdd33d7bb7cafa5c8097e0d5078e789e883 with x0, x1, x2, x3, x4 leaving 7 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

■

Proofgold Proof