Let X, Y and U be given.
Assume HUsub: U ⊆ X.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ preimage_of (setprod X Y) (projection1 X Y) U.
We will prove p ∈ rectangle_set U Y.
We prove the intermediate claim HpXY: p ∈ setprod X Y.
An exact proof term for the current goal is (SepE1 (setprod X Y) (λq ⇒ apply_fun (projection1 X Y) q ∈ U) p Hp).
We prove the intermediate claim HprojU: apply_fun (projection1 X Y) p ∈ U.
An exact proof term for the current goal is (SepE2 (setprod X Y) (λq ⇒ apply_fun (projection1 X Y) q ∈ U) p Hp).
We prove the intermediate claim Happ: apply_fun (projection1 X Y) p = p 0.
An exact proof term for the current goal is (projection1_apply X Y p HpXY).
We prove the intermediate claim Hp0U: p 0 ∈ U.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HprojU.
We prove the intermediate claim Hp1Y: p 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ Y) p HpXY).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta X Y p HpXY).
rewrite the current goal using Heta (from left to right).
An exact proof term for the current goal is (tuple_2_rectangle_set U Y (p 0) (p 1) Hp0U Hp1Y).
Let p be given.
Assume Hp: p ∈ rectangle_set U Y.
We will prove p ∈ preimage_of (setprod X Y) (projection1 X Y) U.
We prove the intermediate claim HpUY: p ∈ setprod U Y.
An exact proof term for the current goal is Hp.
We prove the intermediate claim Hp0U: p 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ Y) p HpUY).
We prove the intermediate claim Hp1Y: p 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ Y) p HpUY).
We prove the intermediate claim Hp0X: p 0 ∈ X.
An exact proof term for the current goal is (HUsub (p 0) Hp0U).
We prove the intermediate claim HpXY: p ∈ setprod X Y.
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta U Y p HpUY).
rewrite the current goal using Heta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (p 0) (p 1) Hp0X Hp1Y).
We prove the intermediate claim Hprop: apply_fun (projection1 X Y) p ∈ U.
We prove the intermediate claim Happ: apply_fun (projection1 X Y) p = p 0.
An exact proof term for the current goal is (projection1_apply X Y p HpXY).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is Hp0U.
An exact proof term for the current goal is (SepI (setprod X Y) (λq ⇒ apply_fun (projection1 X Y) q ∈ U) p HpXY Hprop).
∎