Let A, X, Y, f, g, U and V be given.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of A (pair_map A f g) (rectangle_set U V).
We will prove a ∈ (preimage_of A f U) ∩ (preimage_of A g V).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (SepE1 A (λa0 : set ⇒ apply_fun (pair_map A f g) a0 ∈ rectangle_set U V) a Ha).
We prove the intermediate claim Himg: apply_fun (pair_map A f g) a ∈ rectangle_set U V.
An exact proof term for the current goal is (SepE2 A (λa0 : set ⇒ apply_fun (pair_map A f g) a0 ∈ rectangle_set U V) a Ha).
We prove the intermediate claim Happ: apply_fun (pair_map A f g) a = (apply_fun f a,apply_fun g a).
An exact proof term for the current goal is (pair_map_apply A X Y f g a HaA).
We prove the intermediate claim HpairIn: (apply_fun f a,apply_fun g a) ∈ rectangle_set U V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is Himg.
We prove the intermediate claim Hfst: (apply_fun f a,apply_fun g a) 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ V) (apply_fun f a,apply_fun g a) HpairIn).
We prove the intermediate claim Hsnd: (apply_fun f a,apply_fun g a) 1 ∈ V.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ V) (apply_fun f a,apply_fun g a) HpairIn).
We prove the intermediate claim HfaU: apply_fun f a ∈ U.
rewrite the current goal using (tuple_2_0_eq (apply_fun f a) (apply_fun g a)) (from right to left).
An exact proof term for the current goal is Hfst.
We prove the intermediate claim HgaV: apply_fun g a ∈ V.
rewrite the current goal using (tuple_2_1_eq (apply_fun f a) (apply_fun g a)) (from right to left).
An exact proof term for the current goal is Hsnd.
Apply binintersectI to the current goal.
An exact proof term for the current goal is (SepI A (λa0 : set ⇒ apply_fun f a0 ∈ U) a HaA HfaU).
An exact proof term for the current goal is (SepI A (λa0 : set ⇒ apply_fun g a0 ∈ V) a HaA HgaV).
Let a be given.
Assume Ha: a ∈ (preimage_of A f U) ∩ (preimage_of A g V).
We will prove a ∈ preimage_of A (pair_map A f g) (rectangle_set U V).
We prove the intermediate claim Haf: a ∈ preimage_of A f U.
An exact proof term for the current goal is (binintersectE1 (preimage_of A f U) (preimage_of A g V) a Ha).
We prove the intermediate claim Hag: a ∈ preimage_of A g V.
An exact proof term for the current goal is (binintersectE2 (preimage_of A f U) (preimage_of A g 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 f a0 ∈ U) a Haf).
We prove the intermediate claim HfaU: apply_fun f a ∈ U.
An exact proof term for the current goal is (SepE2 A (λa0 : set ⇒ apply_fun f a0 ∈ U) a Haf).
We prove the intermediate claim HgaV: apply_fun g a ∈ V.
An exact proof term for the current goal is (SepE2 A (λa0 : set ⇒ apply_fun g a0 ∈ V) a Hag).
We prove the intermediate claim HpairIn: (apply_fun f a,apply_fun g a) ∈ rectangle_set U V.
An exact proof term for the current goal is (tuple_2_rectangle_set U V (apply_fun f a) (apply_fun g a) HfaU HgaV).
We prove the intermediate claim Happ: apply_fun (pair_map A f g) a = (apply_fun f a,apply_fun g a).
An exact proof term for the current goal is (pair_map_apply A X Y f g a HaA).
We prove the intermediate claim Himg: apply_fun (pair_map A f g) a ∈ rectangle_set U V.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HpairIn.
An exact proof term for the current goal is (SepI A (λa0 : set ⇒ apply_fun (pair_map A f g) a0 ∈ rectangle_set U V) a HaA Himg).
∎