Let x0 of type ι be given.
Let x1 of type ι be given.
Apply set_ext with
x1,
lam x0 (λ x2 . ap x1 x2) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H1: x2 ∈ x1.
Apply H0 with
x2,
x2 ∈ lam x0 (λ x3 . ap x1 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H2:
(λ x4 . and (x4 ∈ x0) (∃ x5 . x2 = setsum x4 x5)) x3.
Apply H2 with
x2 ∈ lam x0 (λ x4 . ap x1 x4).
Assume H3: x3 ∈ x0.
Assume H4:
∃ x4 . x2 = setsum x3 x4.
Apply H4 with
x2 ∈ lam x0 (λ x4 . ap x1 x4).
Let x4 of type ι be given.
Apply H5 with
λ x5 x6 . x6 ∈ lam x0 (λ x7 . ap x1 x7).
Apply lamI with
x0,
λ x5 . ap x1 x5,
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply apI with
x1,
x3,
x4.
Apply H5 with
λ x5 x6 . x5 ∈ x1.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H1:
x2 ∈ lam x0 (λ x3 . ap x1 x3).
Apply lamE with
x0,
λ x3 . ap x1 x3,
x2,
x2 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H2:
(λ x4 . and (x4 ∈ x0) (∃ x5 . and (x5 ∈ ap x1 x4) (x2 = setsum x4 x5))) x3.
Apply H2 with
x2 ∈ x1.
Assume H3: x3 ∈ x0.
Assume H4:
∃ x4 . and (x4 ∈ ap x1 x3) (x2 = setsum x3 x4).
Apply H4 with
x2 ∈ x1.
Let x4 of type ι be given.
Assume H5:
(λ x5 . and (x5 ∈ ap x1 x3) (x2 = setsum x3 x5)) x4.
Apply H5 with
x2 ∈ x1.
Assume H6:
x4 ∈ ap x1 x3.
Apply H7 with
λ x5 x6 . x6 ∈ x1.
Apply apE with
x1,
x3,
x4.
The subproof is completed by applying H6.