Let A, X, Y, h, U and V be given.
Assume Hh: function_on h A (setprod X Y).
Assume HU: U ⊆ X.
Assume HV: V ⊆ Y.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of A h (rectangle_set U V).
We will prove a ∈ (preimage_of A (compose_fun A h (projection_map1 X Y)) U) ∩ (preimage_of A (compose_fun A h (projection_map2 X Y)) V).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (SepE1 A (λa0 : set ⇒ apply_fun h a0 ∈ rectangle_set U V) a Ha).
We prove the intermediate claim Himg: apply_fun h a ∈ rectangle_set U V.
An exact proof term for the current goal is (SepE2 A (λa0 : set ⇒ apply_fun h a0 ∈ rectangle_set U V) a Ha).
We prove the intermediate claim HpXY: apply_fun h a ∈ setprod X Y.
An exact proof term for the current goal is (Hh a HaA).
We prove the intermediate claim Hp0U: (apply_fun h a) 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ V) (apply_fun h a) Himg).
We prove the intermediate claim Hp1V: (apply_fun h a) 1 ∈ V.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ V) (apply_fun h a) Himg).
We prove the intermediate claim Happ1: apply_fun (projection_map1 X Y) (apply_fun h a) = (apply_fun h a) 0.
An exact proof term for the current goal is (projection1_apply X Y (apply_fun h a) HpXY).
We prove the intermediate claim Happ2: apply_fun (projection_map2 X Y) (apply_fun h a) = (apply_fun h a) 1.
An exact proof term for the current goal is (projection2_apply X Y (apply_fun h a) HpXY).
We prove the intermediate claim Hc1: apply_fun (compose_fun A h (projection_map1 X Y)) a ∈ U.
We prove the intermediate claim Hcomp: apply_fun (compose_fun A h (projection_map1 X Y)) a = apply_fun (projection_map1 X Y) (apply_fun h a).
An exact proof term for the current goal is (compose_fun_apply A h (projection_map1 X Y) a HaA).
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using Happ1 (from left to right).
An exact proof term for the current goal is Hp0U.
We prove the intermediate claim Hc2: apply_fun (compose_fun A h (projection_map2 X Y)) a ∈ V.
We prove the intermediate claim Hcomp: apply_fun (compose_fun A h (projection_map2 X Y)) a = apply_fun (projection_map2 X Y) (apply_fun h a).
An exact proof term for the current goal is (compose_fun_apply A h (projection_map2 X Y) a HaA).
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using Happ2 (from left to right).
An exact proof term for the current goal is Hp1V.
Apply binintersectI to the current goal.
An exact proof term for the current goal is (SepI A (λa0 : set ⇒ apply_fun (compose_fun A h (projection_map1 X Y)) a0 ∈ U) a HaA Hc1).
An exact proof term for the current goal is (SepI A (λa0 : set ⇒ apply_fun (compose_fun A h (projection_map2 X Y)) a0 ∈ V) a HaA Hc2).
Let a be given.
Assume Ha: a ∈ (preimage_of A (compose_fun A h (projection_map1 X Y)) U) ∩ (preimage_of A (compose_fun A h (projection_map2 X Y)) V).
We will prove a ∈ preimage_of A h (rectangle_set U V).
We prove the intermediate claim Ha1: a ∈ preimage_of A (compose_fun A h (projection_map1 X Y)) U.
An exact proof term for the current goal is (binintersectE1 (preimage_of A (compose_fun A h (projection_map1 X Y)) U) (preimage_of A (compose_fun A h (projection_map2 X Y)) V) a Ha).
We prove the intermediate claim Ha2: a ∈ preimage_of A (compose_fun A h (projection_map2 X Y)) V.
An exact proof term for the current goal is (binintersectE2 (preimage_of A (compose_fun A h (projection_map1 X Y)) U) (preimage_of A (compose_fun A h (projection_map2 X Y)) V) a Ha).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (SepE1 A (λa0 : set ⇒ apply_fun (compose_fun A h (projection_map1 X Y)) a0 ∈ U) a Ha1).
We prove the intermediate claim HpXY: apply_fun h a ∈ setprod X Y.
An exact proof term for the current goal is (Hh a HaA).
We prove the intermediate claim Hc1: apply_fun (compose_fun A h (projection_map1 X Y)) a ∈ U.
An exact proof term for the current goal is (SepE2 A (λa0 : set ⇒ apply_fun (compose_fun A h (projection_map1 X Y)) a0 ∈ U) a Ha1).
We prove the intermediate claim Hc2: apply_fun (compose_fun A h (projection_map2 X Y)) a ∈ V.
An exact proof term for the current goal is (SepE2 A (λa0 : set ⇒ apply_fun (compose_fun A h (projection_map2 X Y)) a0 ∈ V) a Ha2).
We prove the intermediate claim Hcomp1: apply_fun (compose_fun A h (projection_map1 X Y)) a = apply_fun (projection_map1 X Y) (apply_fun h a).
An exact proof term for the current goal is (compose_fun_apply A h (projection_map1 X Y) a HaA).
We prove the intermediate claim Hcomp2: apply_fun (compose_fun A h (projection_map2 X Y)) a = apply_fun (projection_map2 X Y) (apply_fun h a).
An exact proof term for the current goal is (compose_fun_apply A h (projection_map2 X Y) a HaA).
We prove the intermediate claim Happ1: apply_fun (projection_map1 X Y) (apply_fun h a) = (apply_fun h a) 0.
An exact proof term for the current goal is (projection1_apply X Y (apply_fun h a) HpXY).
We prove the intermediate claim Happ2: apply_fun (projection_map2 X Y) (apply_fun h a) = (apply_fun h a) 1.
An exact proof term for the current goal is (projection2_apply X Y (apply_fun h a) HpXY).
We prove the intermediate claim Hp0U: (apply_fun h a) 0 ∈ U.
rewrite the current goal using Happ1 (from right to left).
rewrite the current goal using Hcomp1 (from right to left).
An exact proof term for the current goal is Hc1.
We prove the intermediate claim Hp1V: (apply_fun h a) 1 ∈ V.
rewrite the current goal using Happ2 (from right to left).
rewrite the current goal using Hcomp2 (from right to left).
An exact proof term for the current goal is Hc2.
We prove the intermediate claim Heta: apply_fun h a = ((apply_fun h a) 0,(apply_fun h a) 1).
An exact proof term for the current goal is (setprod_eta X Y (apply_fun h a) HpXY).
We prove the intermediate claim HpUV: apply_fun h a ∈ setprod U V.
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 U V ((apply_fun h a) 0) ((apply_fun h a) 1) Hp0U Hp1V).
We will prove a ∈ preimage_of A h (rectangle_set U V).
An exact proof term for the current goal is (SepI A (λa0 : set ⇒ apply_fun h a0 ∈ rectangle_set U V) a HaA HpUV).
∎