Let X, Y, U and V be given.
Assume HUsub: U ⊆ X.
Assume HVsub: V ⊆ Y.
Assume HUne: U ≠ Empty.
Set x0 to be the term Eps_i (λx : set ⇒ x ∈ U).
We prove the intermediate claim Hexx: ∃x : set, x ∈ U.
An exact proof term for the current goal is (nonempty_has_element U HUne).
We prove the intermediate claim Hx0: x0 ∈ U.
An exact proof term for the current goal is (Eps_i_ex (λx : set ⇒ x ∈ U) Hexx).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ projection_image2 X Y (setprod U V).
We will prove y ∈ V.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ setprod U V) y Hy).
We prove the intermediate claim Hex: ∃x : set, (x,y) ∈ setprod U V.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ setprod U V) y Hy).
Apply Hex to the current goal.
Let x be given.
Assume Hxy: (x,y) ∈ setprod U V.
We prove the intermediate claim Hy1: ((x,y) 1) ∈ V.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ V) (x,y) Hxy).
rewrite the current goal using (tuple_2_1_eq x y) (from right to left).
An exact proof term for the current goal is Hy1.
Let y be given.
Assume HyV: y ∈ V.
We will prove y ∈ projection_image2 X Y (setprod U V).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (HVsub y HyV).
We prove the intermediate claim Hpred: ∃x : set, (x,y) ∈ setprod U V.
We use x0 to witness the existential quantifier.
An exact proof term for the current goal is (lamI2 U (λ_ : set ⇒ V) x0 Hx0 y HyV).
An exact proof term for the current goal is (SepI Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ setprod U V) y HyY Hpred).
∎