Let X, Y and V be given.
Assume HVsub: V ⊆ Y.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ preimage_of (setprod X Y) (projection2 X Y) V.
We will prove p ∈ rectangle_set X V.
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 (projection2 X Y) q ∈ V) p Hp).
We prove the intermediate claim HprojV: apply_fun (projection2 X Y) p ∈ V.
An exact proof term for the current goal is (SepE2 (setprod X Y) (λq ⇒ apply_fun (projection2 X Y) q ∈ V) p Hp).
We prove the intermediate claim Happ: apply_fun (projection2 X Y) p = p 1.
An exact proof term for the current goal is (projection2_apply X Y p HpXY).
We prove the intermediate claim Hp1V: p 1 ∈ V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HprojV.
We prove the intermediate claim Hp0X: p 0 ∈ X.
An exact proof term for the current goal is (ap0_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 X V (p 0) (p 1) Hp0X Hp1V).
Let p be given.
Assume Hp: p ∈ rectangle_set X V.
We will prove p ∈ preimage_of (setprod X Y) (projection2 X Y) V.
We prove the intermediate claim HpXV: p ∈ setprod X V.
An exact proof term for the current goal is Hp.
We prove the intermediate claim Hp0X: p 0 ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ V) p HpXV).
We prove the intermediate claim Hp1V: p 1 ∈ V.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ V) p HpXV).
We prove the intermediate claim Hp1Y: p 1 ∈ Y.
An exact proof term for the current goal is (HVsub (p 1) Hp1V).
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 X V p HpXV).
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 (projection2 X Y) p ∈ V.
We prove the intermediate claim Happ: apply_fun (projection2 X Y) p = p 1.
An exact proof term for the current goal is (projection2_apply X Y p HpXY).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is Hp1V.
An exact proof term for the current goal is (SepI (setprod X Y) (λq ⇒ apply_fun (projection2 X Y) q ∈ V) p HpXY Hprop).
∎