Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply set_ext with
setsum x0 (binunion x1 x2),
binunion (setsum x0 x1) {Inj1 x3|x3 ∈ x2} leaving 2 subgoals.
Let x3 of type ι be given.
Apply setsum_Inj_inv with
x0,
binunion x1 x2,
x3,
x3 ∈ binunion (setsum x0 x1) {Inj1 x4|x4 ∈ x2} leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1:
∃ x4 . and (x4 ∈ x0) (x3 = Inj0 x4).
Apply H1 with
x3 ∈ binunion (setsum x0 x1) {Inj1 x4|x4 ∈ x2}.
Let x4 of type ι be given.
Assume H2:
(λ x5 . and (x5 ∈ x0) (x3 = Inj0 x5)) x4.
Apply H2 with
x3 ∈ binunion (setsum x0 x1) {Inj1 x5|x5 ∈ x2}.
Assume H3: x4 ∈ x0.
Apply binunionI1 with
setsum x0 x1,
{Inj1 x5|x5 ∈ x2},
x3.
Apply H4 with
λ x5 x6 . x6 ∈ setsum x0 x1.
Apply Inj0_setsum with
x0,
x1,
x4.
The subproof is completed by applying H3.
Apply H1 with
x3 ∈ binunion (setsum x0 x1) {Inj1 x4|x4 ∈ x2}.
Let x4 of type ι be given.
Apply H2 with
x3 ∈ binunion (setsum x0 x1) {Inj1 x5|x5 ∈ x2}.
Apply binunionE with
x1,
x2,
x4,
x3 ∈ binunion (setsum x0 x1) {Inj1 x5|x5 ∈ x2} leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H5: x4 ∈ x1.
Apply binunionI1 with
setsum x0 x1,
{Inj1 x5|x5 ∈ x2},
x3.
Apply H4 with
λ x5 x6 . x6 ∈ setsum x0 x1.
Apply Inj1_setsum with
x0,
x1,
x4.
The subproof is completed by applying H5.
Assume H5: x4 ∈ x2.
Apply binunionI2 with
setsum x0 x1,
{Inj1 x5|x5 ∈ x2},
x3.
Apply H4 with
λ x5 x6 . x6 ∈ {Inj1 x7|x7 ∈ x2}.
Apply ReplI with
x2,
Inj1,
x4.
The subproof is completed by applying H5.
Let x3 of type ι be given.
Apply binunionE with
setsum x0 x1,
{Inj1 x4|x4 ∈ x2},
x3,
x3 ∈ setsum x0 (binunion x1 x2) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply setsum_Inj_inv with
x0,
x1,
x3,
x3 ∈ setsum x0 (binunion x1 x2) leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2:
∃ x4 . and (x4 ∈ x0) (x3 = Inj0 x4).
Apply H2 with
x3 ∈ setsum x0 (binunion x1 x2).
Let x4 of type ι be given.
Assume H3:
(λ x5 . and (x5 ∈ ...) ...) ....