Let Y and x0 be given.
Set idY to be the term {(y,y)|y ∈ Y}.
We will prove image_of (pair_map Y (const_fun Y x0) idY) Y = setprod {x0} Y.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ image_of (pair_map Y (const_fun Y x0) idY) Y.
We will prove p ∈ setprod {x0} Y.
Set f to be the term pair_map Y (const_fun Y x0) idY.
We prove the intermediate claim HpRepl: p ∈ Repl Y (λa ⇒ apply_fun f a).
An exact proof term for the current goal is Hp.
Apply (ReplE_impred Y (λa : set ⇒ apply_fun f a) p HpRepl) to the current goal.
Let a be given.
Assume HaY: a ∈ Y.
Assume Heq: p = apply_fun f a.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hfa: apply_fun f a = (apply_fun (const_fun Y x0) a,apply_fun idY a).
An exact proof term for the current goal is (pair_map_apply Y {x0} Y (const_fun Y x0) idY a HaY).
We prove the intermediate claim Hc: apply_fun (const_fun Y x0) a = x0.
An exact proof term for the current goal is (const_fun_apply Y x0 a HaY).
We prove the intermediate claim Hid: apply_fun idY a = a.
An exact proof term for the current goal is (identity_function_apply Y a HaY).
rewrite the current goal using Hfa (from left to right).
rewrite the current goal using Hc (from left to right).
rewrite the current goal using Hid (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x0} Y x0 a (SingI x0) HaY).
Let p be given.
Assume Hp: p ∈ setprod {x0} Y.
We will prove p ∈ image_of (pair_map Y (const_fun Y x0) idY) Y.
Set f to be the term pair_map Y (const_fun Y x0) idY.
We prove the intermediate claim Hp0Sing: (p 0) ∈ {x0}.
An exact proof term for the current goal is (ap0_Sigma {x0} (λ_ : set ⇒ Y) p Hp).
We prove the intermediate claim Hp1Y: (p 1) ∈ Y.
An exact proof term for the current goal is (ap1_Sigma {x0} (λ_ : set ⇒ Y) p Hp).
We prove the intermediate claim Hp0eq: (p 0) = x0.
An exact proof term for the current goal is (singleton_elem (p 0) x0 Hp0Sing).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta {x0} Y p Hp).
We will prove p ∈ Repl Y (λa ⇒ apply_fun f a).
We prove the intermediate claim Hfp1: apply_fun f (p 1) = (apply_fun (const_fun Y x0) (p 1),apply_fun idY (p 1)).
An exact proof term for the current goal is (pair_map_apply Y {x0} Y (const_fun Y x0) idY (p 1) Hp1Y).
We prove the intermediate claim Hc1: apply_fun (const_fun Y x0) (p 1) = x0.
An exact proof term for the current goal is (const_fun_apply Y x0 (p 1) Hp1Y).
We prove the intermediate claim Hid1: apply_fun idY (p 1) = (p 1).
An exact proof term for the current goal is (identity_function_apply Y (p 1) Hp1Y).
We prove the intermediate claim Hfp1eq: apply_fun f (p 1) = (p 0,p 1).
rewrite the current goal using Hfp1 (from left to right).
rewrite the current goal using Hc1 (from left to right).
rewrite the current goal using Hid1 (from left to right).
rewrite the current goal using Hp0eq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hp_as_image: p = apply_fun f (p 1).
rewrite the current goal using Heta (from left to right) at position 1.
rewrite the current goal using Hfp1eq (from right to left).
Use reflexivity.
rewrite the current goal using Hp_as_image (from left to right).
An exact proof term for the current goal is (ReplI Y (λa : set ⇒ apply_fun f a) (p 1) Hp1Y).
∎