Let X, Y, U and V be given.
Assume HUsub: U ⊆ X.
Assume HVsub: V ⊆ Y.
Assume HVne: V ≠ Empty.
Set y0 to be the term Eps_i (λy : set ⇒ y ∈ V).
We prove the intermediate claim Hexy: ∃y : set, y ∈ V.
An exact proof term for the current goal is (nonempty_has_element V HVne).
We prove the intermediate claim Hy0: y0 ∈ V.
An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ y ∈ V) Hexy).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ projection_image1 X Y (setprod U V).
We will prove x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ setprod U V) x Hx).
We prove the intermediate claim Hex: ∃y : set, (x,y) ∈ setprod U V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ setprod U V) x Hx).
Apply Hex to the current goal.
Let y be given.
Assume Hxy: (x,y) ∈ setprod U V.
We prove the intermediate claim Hx0: ((x,y) 0) ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ V) (x,y) Hxy).
rewrite the current goal using (tuple_2_0_eq x y) (from right to left).
An exact proof term for the current goal is Hx0.
Let x be given.
Assume HxU: x ∈ U.
We will prove x ∈ projection_image1 X Y (setprod U V).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsub x HxU).
We prove the intermediate claim Hpred: ∃y : set, (x,y) ∈ setprod U V.
We use y0 to witness the existential quantifier.
An exact proof term for the current goal is (lamI2 U (λ_ : set ⇒ V) x HxU y0 Hy0).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ setprod U V) x HxX Hpred).
∎