Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x0 ⊆ x1.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι be given.
Assume H1: ∀ x4 . x4 ∈ x0 ⟶ x2 x4 ⊆ x3 x4.
Let x4 of type ι be given.
Assume H2:
x4 ∈ lam x0 (λ x5 . x2 x5).
Apply and3E with
setsum (proj0 x4) (proj1 x4) = x4,
proj0 x4 ∈ x0,
proj1 x4 ∈ x2 (proj0 x4),
x4 ∈ lam x1 x3 leaving 2 subgoals.
Apply Sigma_eta_proj0_proj1 with
x0,
x2,
x4.
The subproof is completed by applying H2.
Assume H4:
proj0 x4 ∈ x0.
Apply H3 with
λ x5 x6 . x5 ∈ lam x1 (λ x7 . x3 x7).
Apply lamI with
x1,
x3,
proj0 x4,
proj1 x4 leaving 2 subgoals.
Apply H0 with
proj0 x4.
The subproof is completed by applying H4.
Apply H1 with
proj0 x4,
proj1 x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.