Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Apply xm with
∃ x3 . and (x3 ∈ x0) (x1 x3),
x2 ∈ {x3 ∈ x0|x1 x3} ⟶ and (x2 ∈ x0) (x1 x2) leaving 2 subgoals.
Assume H0:
∃ x3 . and (x3 ∈ x0) (x1 x3).
Claim L1:
If_i (∃ x3 . and (x3 ∈ x0) (x1 x3)) {(λ x4 . If_i (x1 x4) x4 (prim0 (λ x5 . and (x5 ∈ x0) (x1 x5)))) x3|x3 ∈ x0} 0 = {(λ x4 . If_i (x1 x4) x4 (prim0 (λ x5 . and (x5 ∈ x0) (x1 x5)))) x3|x3 ∈ x0}Apply If_i_1 with
∃ x3 . and (x3 ∈ x0) (x1 x3),
{(λ x4 . If_i (x1 x4) x4 (prim0 (λ x5 . and (x5 ∈ x0) (x1 x5)))) x3|x3 ∈ x0},
0.
The subproof is completed by applying H0.
Apply L1 with
λ x3 x4 . x2 ∈ x4 ⟶ and (x2 ∈ x0) (x1 x2).
Assume H2:
x2 ∈ {(λ x4 . If_i (x1 x4) x4 (prim0 (λ x5 . and (x5 ∈ x0) (x1 x5)))) x3|x3 ∈ x0}.
Apply ReplE_impred with
x0,
λ x3 . If_i (x1 x3) x3 (prim0 (λ x4 . and (x4 ∈ x0) (x1 x4))),
x2,
and (x2 ∈ x0) (x1 x2) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H3: x3 ∈ x0.
Assume H4:
x2 = (λ x4 . If_i (x1 x4) x4 (prim0 (λ x5 . and (x5 ∈ x0) (x1 x5)))) x3.
Apply xm with
x1 x3,
and (x2 ∈ x0) (x1 x2) leaving 2 subgoals.
Assume H5: x1 x3.
Claim L6: x2 = x3
Apply If_i_1 with
x1 x3,
x3,
prim0 (λ x4 . and (x4 ∈ x0) (x1 x4)),
λ x4 x5 . x2 = x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Apply L6 with
λ x4 x5 . and (x5 ∈ x0) (x1 x5).
Apply andI with
x3 ∈ x0,
x1 x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
Claim L6:
x2 = prim0 (λ x4 . and (x4 ∈ x0) (x1 x4))Apply If_i_0 with
x1 x3,
x3,
prim0 (λ x4 . and (x4 ∈ x0) (x1 x4)),
λ x4 x5 . x2 = x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Apply L6 with
λ x4 x5 . and (x5 ∈ x0) (x1 x5).
Apply Eps_i_ex with
λ x4 . and (x4 ∈ x0) (x1 x4).
The subproof is completed by applying H0.
Assume H0:
not (∃ x3 . and (x3 ∈ x0) (x1 x3)).
Apply L1 with
λ x3 x4 . x2 ∈ x4 ⟶ and (x2 ∈ x0) (x1 x2).