Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Assume H1:
∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3).
Assume H2:
∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)).
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply setminusE with
u18,
binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1),
x2,
4b3fa.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1) leaving 2 subgoals.
The subproof is completed by applying H4.
Claim L7: x1 = x2 ⟶ ∀ x3 : ο . x3
Apply Eps_i_ex with
λ x3 . x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1).
Apply unknownprop_a7eebbd0877028a5b64563f3f8deb69ec800c19cc86ab34abae3b4eaf878db79 with
x0,
x2,
x1,
∃ x3 . x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1) leaving 8 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
Apply neq_i_sym with
x1,
x2.
The subproof is completed by applying L7.
Assume H8: x0 x2 x1.
Apply H6.
Apply binunionI1 with
DirGraphOutNeighbors u18 x0 x1,
Sing x1,
x2.
Apply SepI with
u18,
λ x3 . and (x1 = x3 ⟶ ∀ x4 : ο . x4) (x0 x1 x3),
x2 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply andI with
x1 = x2 ⟶ ∀ x3 : ο . x3,
x0 x1 x2 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply H0 with
x2,
x1.
The subproof is completed by applying H8.
Let x3 of type ι → ι be given.