Let x0 of type ι be given.
Apply SepI with
setexp x0 x0,
λ x1 . bij x0 x0 (λ x2 . ap x1 x2),
lam x0 (λ x1 . x1) leaving 2 subgoals.
Apply lam_Pi with
x0,
λ x1 . x0,
λ x1 . x1.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
The subproof is completed by applying H0.
Apply and3I with
∀ x1 . x1 ∈ x0 ⟶ ap (lam x0 (λ x2 . x2)) x1 ∈ x0,
∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 (λ x3 . x3)) x1 = ap (lam x0 (λ x3 . x3)) x2 ⟶ x1 = x2,
∀ x1 . x1 ∈ x0 ⟶ ∃ x2 . and (x2 ∈ x0) (ap (lam x0 (λ x3 . x3)) x2 = x1) leaving 3 subgoals.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Apply beta with
x0,
λ x2 . x2,
x1,
λ x2 x3 . x3 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Let x2 of type ι be given.
Assume H1: x2 ∈ x0.
Apply beta with
x0,
λ x3 . x3,
x1,
λ x3 x4 . x4 = ap (lam x0 (λ x5 . x5)) x2 ⟶ x1 = x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply beta with
x0,
λ x3 . x3,
x2,
λ x3 x4 . x1 = x4 ⟶ x1 = x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: x1 = x2.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Let x2 of type ο be given.
Assume H1:
∀ x3 . and (x3 ∈ x0) (ap (lam x0 (λ x4 . x4)) x3 = x1) ⟶ x2.
Apply H1 with
x1.
Apply andI with
x1 ∈ x0,
ap (lam x0 (λ x3 . x3)) x1 = x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply beta with
x0,
λ x3 . x3,
x1.
The subproof is completed by applying H0.