Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Assume H0:
∀ x3 . x3 ∈ x2 ⟶ and (pair_p x3) (ap x3 0 ∈ x0).
Assume H1:
∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3.
Apply SepI with
prim4 (lam x0 (λ x3 . prim3 (x1 x3))),
λ x3 . ∀ x4 . x4 ∈ x0 ⟶ ap x3 x4 ∈ x1 x4,
x2 leaving 2 subgoals.
Apply PowerI with
lam x0 (λ x3 . prim3 (x1 x3)),
x2.
Let x3 of type ι be given.
Assume H2: x3 ∈ x2.
Apply H0 with
x3,
x3 ∈ lam x0 (λ x4 . prim3 (x1 x4)) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H3 with
λ x4 x5 . x4 ∈ lam x0 (λ x6 . prim3 (x1 x6)).
Apply lamI with
x0,
λ x4 . prim3 (x1 x4),
ap x3 0,
ap x3 1 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply UnionI with
x1 (ap x3 0),
ap x3 1,
ap x2 (ap x3 0) leaving 2 subgoals.
Apply apI with
x2,
ap x3 0,
ap x3 1.
Apply H3 with
λ x4 x5 . x5 ∈ x2.
The subproof is completed by applying H2.
Apply H1 with
ap x3 0.
The subproof is completed by applying H4.
The subproof is completed by applying H1.