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)}.
Apply SepE with
setexp x0 x0,
λ x2 . bij x0 x0 (λ x3 . ap x2 x3),
x1,
and (and (lam x0 (λ x2 . inv x0 (λ x3 . ap x1 x3) x2) ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)}) (lam x0 (λ x2 . ap (lam x0 (λ x3 . inv x0 (λ x4 . ap x1 x4) x3)) (ap x1 x2)) = lam x0 (λ x2 . x2))) (lam x0 (λ x2 . ap x1 (ap (lam x0 (λ x3 . inv x0 (λ x4 . ap x1 x4) x3)) x2)) = lam x0 (λ x2 . x2)) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2:
bij x0 x0 (λ x2 . ap x1 x2).
Apply and3I with
lam x0 (λ x2 . inv x0 (λ x3 . ap x1 x3) x2) ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)},
lam x0 (λ x2 . ap (lam x0 (λ x3 . inv x0 (λ x4 . ap x1 x4) x3)) (ap x1 x2)) = lam x0 (λ x2 . x2),
lam x0 (λ x2 . ap x1 (ap (lam x0 (λ x3 . inv x0 (λ x4 . ap x1 x4) x3)) x2)) = lam x0 (λ x2 . x2) leaving 3 subgoals.
Apply SepI with
setexp x0 x0,
λ x2 . bij x0 x0 (λ x3 . ap x2 x3),
lam x0 (λ x2 . inv x0 (λ x3 . ap x1 x3) x2) leaving 2 subgoals.
Apply lam_Pi with
x0,
λ x2 . x0,
λ x2 . inv x0 (λ x3 . ap x1 x3) x2.
The subproof is completed by applying L7.
Apply and3I with
∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 (λ x3 . inv x0 (λ x4 . ap x1 x4) x3)) x2 ∈ x0,
∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ap (lam x0 (λ x4 . inv x0 (λ x5 . ap x1 x5) x4)) x2 = ap (lam x0 (λ x4 . inv x0 (λ x5 . ap x1 x5) x4)) x3 ⟶ x2 = x3,
∀ x2 . ... ⟶ ∃ x3 . and (x3 ∈ ...) ... leaving 3 subgoals.