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.

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H4: x3 ∈ x0.

Assume H5: x4 ∈ DirGraphOutNeighbors x0 x1 x3.

Assume H6: ∀ 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).

Let x5 of type ι → ι be given.

Assume H8: ∀ x6 . x6 ∈ {x7 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x3)) x2} ⟶ ∀ x7 . x7 ∈ DirGraphOutNeighbors x0 x1 x3 ⟶ x1 x7 x6 ⟶ x7 = x5 x6.

Apply unknownprop_00264abf93bf449ce6ca0d70eac26610b57a2f2e3100fbb92347a47265872147 with x0, x1, x2, x3, x4, x5 leaving 6 subgoals.

The subproof is completed by applying H0.

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