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.
Assume H5: x1 = x2 ⟶ ∀ x3 : ο . x3.
Assume H6:
not (x0 x1 x2).
Apply dneg with
atleastp u1 (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)).
Apply H2 with
binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x2) leaving 3 subgoals.
Apply binunion_Subq_min with
DirGraphOutNeighbors u18 x0 x1,
Sing x2,
u18 leaving 2 subgoals.
The subproof is completed by applying Sep_Subq with
u18,
λ x3 . and (x1 = x3 ⟶ ∀ x4 : ο . x4) (x0 x1 x3).
Let x3 of type ι be given.
Apply SingE with
x2,
x3,
λ x4 x5 . x5 ∈ u18 leaving 2 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H4.
Apply atleastp_tra with
u6,
setsum u5 u1,
binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x2) leaving 2 subgoals.
Apply equip_atleastp with
u6,
setsum u5 u1.
Apply unknownprop_cbcdc516d918dc788420402237ec548f378f3cef789b7403c9dd8f4b8490ac8e with
λ x3 x4 . equip x3 (setsum u5 u1).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
u5,
u1,
u5,
u1 leaving 4 subgoals.
The subproof is completed by applying nat_5.
The subproof is completed by applying nat_1.
The subproof is completed by applying equip_ref with
u5.
The subproof is completed by applying equip_ref with
u1.
Apply unknownprop_f59d6b770984c869c1e5c6fa6c966bf2e7f31a21d93561635565b3e8dc0de299 with
u5,
u1,
DirGraphOutNeighbors u18 x0 x1,
Sing x2 leaving 3 subgoals.
Apply equip_atleastp with
u5,
DirGraphOutNeighbors u18 x0 x1.
Apply equip_sym with
DirGraphOutNeighbors u18 x0 x1,
u5.
Apply unknownprop_942eb02a74c10f16602e1ae1f344c3023e05004e91bcaa34f489f7c49867be93 with
x0,
x1 leaving 4 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 H3.
Apply unknownprop_12ee6633dc54fc9da79764260fff4b3b0c4c52c79582045c211dac0d55037713 with
Sing x2,
x2.
The subproof is completed by applying SingI with x2.
Let x3 of type ι be given.
Assume H10:
x3 ∈ Sing x2.
Apply L8.
Apply SingE with
x2,
x3,
λ x4 x5 . x4 ∈ DirGraphOutNeighbors u18 x0 x1 leaving 2 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H9.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply binunionE with
DirGraphOutNeighbors u18 x0 x1,
Sing x2,
x3,
(x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x0 x3 x4) leaving 3 subgoals.
The subproof is completed by applying H9.