Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H3: x3 = x4 ⟶ ∀ x7 : ο . x7.
Assume H6:
∀ x7 . x7 ∈ x1 ⟶ or (equip {x8 ∈ x0|x2 x8 = x7} x3) (equip {x8 ∈ x0|x2 x8 = x7} x4).
Assume H7:
equip {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} x5.
Assume H8:
equip {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4} x6.
Apply unknownprop_8e052d85b2d476997756a4d2563048c027eabd3d70c30d840e8aa53708c6c883 with
add_nat x5 x6,
x1 leaving 3 subgoals.
Apply add_nat_p with
x5,
x6 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
Apply equip_tra with
add_nat x5 x6,
binunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4},
x1 leaving 2 subgoals.
Apply equip_tra with
add_nat x5 x6,
setsum x5 x6,
binunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4} leaving 2 subgoals.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
x5,
x6,
x5,
x6 leaving 4 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying equip_ref with x5.
The subproof is completed by applying equip_ref with x6.
Apply equip_sym with
binunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4},
setsum x5 x6.
Apply unknownprop_8fed54475e70b18fbe9db03f1a81cd38ab9b210f0bea8d2bb706323c288b83da with
{x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3},
{x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4},
x5,
x6 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
Let x7 of type ι be given.
Assume H9:
x7 ∈ {x8 ∈ x1|equip {x9 ∈ x0|x2 x9 = x8} x3}.
Assume H10:
x7 ∈ {x8 ∈ x1|equip {x9 ∈ x0|x2 x9 = x8} x4}.
Apply SepE with
x1,
λ x8 . equip {x9 ∈ x0|x2 x9 = x8} x3,
x7,
False leaving 2 subgoals.
The subproof is completed by applying H9.
Assume H11: x7 ∈ x1.
Assume H12:
equip {x8 ∈ x0|x2 x8 = x7} x3.
Apply H3.
Apply unknownprop_8e052d85b2d476997756a4d2563048c027eabd3d70c30d840e8aa53708c6c883 with
x3,
x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply equip_tra with
x3,
{x8 ∈ x0|x2 x8 = x7},
x4 leaving 2 subgoals.
Apply equip_sym with
{x8 ∈ x0|x2 x8 = x7},
x3.
The subproof is completed by applying H12.
Apply SepE2 with
x1,
λ x8 . equip {x9 ∈ x0|x2 x9 = x8} x4,
x7.
The subproof is completed by applying H10.
Claim L9:
binunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4} = ...Apply L9 with
λ x7 x8 . equip x8 x1.
The subproof is completed by applying equip_ref with x1.