Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
x1 ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)}.
Let x2 of type ι be given.
Assume H1:
x2 ∈ {x3 ∈ setexp x0 x0|bij x0 x0 (λ x4 . ap x3 x4)}.
Apply SepE with
setexp x0 x0,
λ x3 . bij x0 x0 (λ x4 . ap x3 x4),
x1,
(λ x3 x4 . lam x0 (λ x5 . ap x4 (ap x3 x5))) x1 x2 ∈ {x3 ∈ setexp x0 x0|bij x0 x0 (λ x4 . ap x3 x4)} leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H3:
bij x0 x0 (λ x3 . ap x1 x3).
Apply SepE with
setexp x0 x0,
λ x3 . bij x0 x0 (λ x4 . ap x3 x4),
x2,
(λ x3 x4 . lam x0 (λ x5 . ap x4 (ap x3 x5))) x1 x2 ∈ {x3 ∈ setexp x0 x0|bij x0 x0 (λ x4 . ap x3 x4)} leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H5:
bij x0 x0 (λ x3 . ap x2 x3).
Apply SepI with
setexp x0 x0,
λ x3 . bij x0 x0 (λ x4 . ap x3 x4),
(λ x3 x4 . lam x0 (λ x5 . ap x4 (ap x3 x5))) x1 x2 leaving 2 subgoals.
Apply lam_Pi with
x0,
λ x3 . x0,
λ x3 . ap x2 (ap x1 x3).
Let x3 of type ι be given.
Assume H12: x3 ∈ x0.
Apply L9 with
ap x1 x3.
Apply L6 with
x3.
The subproof is completed by applying H12.
Apply and3I with
∀ x3 . x3 ∈ x0 ⟶ ap (lam x0 (λ x4 . ap x2 (ap x1 x4))) x3 ∈ x0,
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ap (lam x0 (λ x5 . ap x2 (ap x1 x5))) x3 = ap (lam x0 (λ x5 . ap x2 (ap x1 x5))) x4 ⟶ x3 = x4,
∀ x3 . x3 ∈ x0 ⟶ ∃ x4 . and (x4 ∈ x0) (ap (lam x0 (λ x5 . ap x2 (ap x1 x5))) x4 = x3) leaving 3 subgoals.
Let x3 of type ι be given.
Assume H12: x3 ∈ x0.
Apply beta with
x0,
λ x4 . ap x2 (ap x1 x4),
x3,
λ x4 x5 . x5 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H12.
Apply L9 with
ap x1 x3.
Apply L6 with
x3.
The subproof is completed by applying H12.
Let x3 of type ι be given.
Assume H12: x3 ∈ x0.
Let x4 of type ι be given.
Assume H13: x4 ∈ x0.
Apply beta with
x0,
λ x5 . ap x2 (ap ... ...),
...,
... leaving 2 subgoals.