Let A, X, Y, f, g and a be given.
Assume Ha: a ∈ A.
We will prove apply_fun (pair_map A f g) a = (apply_fun f a,apply_fun g a).
We will prove Eps_i (λz ⇒ (a,z) ∈ pair_map A f g) = (apply_fun f a,apply_fun g a).
We prove the intermediate claim H1: (a,(apply_fun f a,apply_fun g a)) ∈ pair_map A f g.
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ (a0,(apply_fun f a0,apply_fun g a0))) a Ha).
We prove the intermediate claim H2: (a,Eps_i (λz ⇒ (a,z) ∈ pair_map A f g)) ∈ pair_map A f g.
An exact proof term for the current goal is (Eps_i_ax (λz ⇒ (a,z) ∈ pair_map A f g) (apply_fun f a,apply_fun g a) H1).
Apply (ReplE_impred A (λa0 : set ⇒ (a0,(apply_fun f a0,apply_fun g a0))) (a,Eps_i (λz ⇒ (a,z) ∈ pair_map A f g)) H2) to the current goal.
Let a0 be given.
Assume Ha0: a0 ∈ A.
Assume Heq: (a,Eps_i (λz ⇒ (a,z) ∈ pair_map A f g)) = (a0,(apply_fun f a0,apply_fun g a0)).
We prove the intermediate claim Ha_eq: a = a0.
rewrite the current goal using (tuple_2_0_eq a (Eps_i (λz ⇒ (a,z) ∈ pair_map A f g))) (from right to left).
rewrite the current goal using (tuple_2_0_eq a0 (apply_fun f a0,apply_fun g a0)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hz_eq: Eps_i (λz ⇒ (a,z) ∈ pair_map A f g) = (apply_fun f a0,apply_fun g a0).
rewrite the current goal using (tuple_2_1_eq a (Eps_i (λz ⇒ (a,z) ∈ pair_map A f g))) (from right to left) at position 1.
rewrite the current goal using (tuple_2_1_eq a0 (apply_fun f a0,apply_fun g a0)) (from right to left) at position 1.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
rewrite the current goal using Hz_eq (from left to right).
rewrite the current goal using Ha_eq (from left to right).
Use reflexivity.
∎