Let x0 of type ι be given.
Apply set_ext with
setprod x0 x0,
setexp x0 2 leaving 2 subgoals.
Let x1 of type ι be given.
Apply and3E with
setsum (proj0 x1) (proj1 x1) = x1,
proj0 x1 ∈ x0,
proj1 x1 ∈ x0,
x1 ∈ setexp x0 2 leaving 2 subgoals.
Apply Sigma_eta_proj0_proj1 with
x0,
λ x2 . x0,
x1.
The subproof is completed by applying H0.
Assume H2:
proj0 x1 ∈ x0.
Assume H3:
proj1 x1 ∈ x0.
Apply H1 with
λ x2 x3 . x2 ∈ setexp x0 2.
Apply tuple_pair with
proj0 x1,
proj1 x1,
λ x2 x3 . x3 ∈ Pi 2 (λ x4 . x0).
Apply lam_Pi with
2,
λ x2 . x0,
λ x2 . If_i (x2 = 0) (proj0 x1) (proj1 x1).
Let x2 of type ι be given.
Assume H4: x2 ∈ 2.
Apply If_i_or with
x2 = 0,
proj0 x1,
proj1 x1,
If_i (x2 = 0) (proj0 x1) (proj1 x1) ∈ x0 leaving 2 subgoals.
Apply H5 with
λ x3 x4 . x4 ∈ x0.
The subproof is completed by applying H2.
Apply H5 with
λ x3 x4 . x4 ∈ x0.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Apply PiE with
2,
λ x2 . x0,
x1,
x1 ∈ setprod x0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1:
∀ x2 . x2 ∈ x1 ⟶ and (pair_p x2) (ap x2 0 ∈ 2).
Assume H2:
∀ x2 . x2 ∈ 2 ⟶ ap x1 x2 ∈ x0.
Apply pair_p_I2 with
x1.
The subproof is completed by applying H1.
Apply L3 with
λ x2 x3 . x2 ∈ setprod x0 x0.
Apply lamI with
x0,
λ x2 . x0,
ap x1 0,
ap x1 1 leaving 2 subgoals.
Apply H2 with
0.
The subproof is completed by applying In_0_2.
Apply H2 with
1.
The subproof is completed by applying In_1_2.