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).

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H2: nat_p x4.

Let x5 of type ι be given.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H3: x5 ⊆ x0.

Assume H4: x6 ⊆ x0.

Assume H5: x7 ⊆ x0.

Assume H6: x5 = setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2).

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

Assume H8: ∀ x8 . x8 ∈ x6 ⟶ nIn x8 x7.

Assume H9: ∀ x8 . x8 ∈ x5 ⟶ nIn x8 x7.

Assume H10: ∀ x8 . x8 ∈ x7 ⟶ x8 ∈ {x9 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x3)) x4}.

Let x8 of type ι be given.

Let x9 of type ι be given.

Assume H11: x8 ∈ x6.

Assume H12: x9 ∈ x7.

Assume H13: x9 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2)).

Assume H14: x1 x8 x9.

Let x10 of type ι → ι be given.

Assume H15: ∀ x11 . x11 ∈ x6 ⟶ x10 x11 ∈ x5.

Assume H16: ∀ x11 . x11 ∈ x6 ⟶ x1 x11 (x10 x11).

Assume H17: ∀ x11 . x11 ∈ x5 ⟶ ∃ x12 . and (x12 ∈ x6) (x10 x12 = x11).

Claim L18: ...

...

Claim L19: ...

...

Claim L20: ...

...

Claim L21: ...

...

Apply atleastp_tra with x4, binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x9), {x11 ∈ setminus x6 (Sing x8)|x1 (x10 x11) x9} leaving 2 subgoals.

The subproof is completed by applying L19.

Let x11 of type ο be given.

Assume H22: ∀ x12 : ι → ι . inj (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x9)) {x13 ∈ setminus x6 (Sing x8)|x1 (x10 x13) x9} x12 ⟶ x11.

Apply H22 with inv x6 x10.

Apply andI with ∀ x12 . x12 ∈ binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x9) ⟶ inv x6 x10 x12 ∈ {x13 ∈ setminus x6 (Sing x8)|x1 (x10 x13) x9}, ∀ x12 . x12 ∈ binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 ... ...) ⟶ ∀ x13 . x13 ∈ binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x9) ⟶ inv x6 x10 x12 = inv x6 x10 x13 ⟶ x12 = x13 leaving 2 subgoals.

...

■

Proofgold Proof