Let A, X, Y, f and g be given.
Assume Hf: function_on f A X.
Assume Hg: function_on g A Y.
We will prove pair_map A f g ∈ function_space A (setprod X Y).
We will prove pair_map A f g ∈ {h ∈ 𝒫 (setprod A (setprod X Y))|function_on h A (setprod X Y)}.
Apply SepI to the current goal.
We will prove pair_map A f g ∈ 𝒫 (setprod A (setprod X Y)).
Apply PowerI to the current goal.
Let z be given.
Assume Hz: z ∈ pair_map A f g.
We will prove z ∈ setprod A (setprod X Y).
Apply (ReplE_impred A (λa0 : set ⇒ (a0,(apply_fun f a0,apply_fun g a0))) z Hz) to the current goal.
Let a0 be given.
Assume Ha0: a0 ∈ A.
Assume Heq: z = (a0,(apply_fun f a0,apply_fun g a0)).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hxy: (apply_fun f a0,apply_fun g a0) ∈ setprod X Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (apply_fun f a0) (apply_fun g a0) (Hf a0 Ha0) (Hg a0 Ha0)).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A (setprod X Y) a0 (apply_fun f a0,apply_fun g a0) Ha0 Hxy).
We will prove function_on (pair_map A f g) A (setprod X Y).
Let a be given.
Assume Ha: a ∈ A.
We will prove apply_fun (pair_map A f g) a ∈ setprod X Y.
rewrite the current goal using (pair_map_apply A X Y f g a Ha) (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (apply_fun f a) (apply_fun g a) (Hf a Ha) (Hg a Ha)).
∎