Let x0 of type ι be given.
Assume H0:
∀ x1 . x1 ∈ x0 ⟶ and (pair_p x1) (ap x1 0 ∈ 2).
Apply set_ext with
setsum {ap x1 1|x1 ∈ x0,setsum 0 (ap x1 1) ∈ x0} {ap x1 1|x1 ∈ x0,setsum 1 (ap x1 1) ∈ x0},
x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply pairE with
{ap x2 1|x2 ∈ x0,setsum 0 (ap x2 1) ∈ x0},
{ap x2 1|x2 ∈ x0,setsum 1 (ap x2 1) ∈ x0},
x1,
x1 ∈ x0 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply exandE_i with
λ x2 . x2 ∈ {ap x3 1|x3 ∈ x0,setsum 0 (ap x3 1) ∈ x0},
λ x2 . x1 = setsum 0 x2,
x1 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H3:
x2 ∈ {ap x3 1|x3 ∈ x0,setsum 0 (ap x3 1) ∈ x0}.
Apply ReplSepE_impred with
x0,
λ x3 . setsum 0 (ap x3 1) ∈ x0,
λ x3 . ap x3 1,
x2,
x1 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H5: x3 ∈ x0.
Apply H4 with
λ x4 x5 . x5 ∈ x0.
Apply H7 with
λ x4 x5 . setsum 0 x5 ∈ x0.
The subproof is completed by applying H6.
Assume H2:
∃ x2 . and (x2 ∈ {ap ... 1|x3 ∈ x0,setsum 1 (ap x3 1) ∈ x0}) ....
Apply L1 with
λ x1 x2 . pair_p x1.
The subproof is completed by applying pair_p_I with
{ap x1 1|x1 ∈ x0,setsum 0 (ap x1 1) ∈ x0},
{ap x1 1|x1 ∈ x0,setsum 1 (ap x1 1) ∈ x0}.