Let X, Y and V be given.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ projection_image2 X Y (setprod Empty V).
We will prove y ∈ Empty.
We prove the intermediate claim Hex: ∃x : set, (x,y) ∈ setprod Empty V.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ setprod Empty V) y Hy).
Apply Hex to the current goal.
Let x be given.
Assume Hxy: (x,y) ∈ setprod Empty V.
We prove the intermediate claim HxEmpty: ((x,y) 0) ∈ Empty.
An exact proof term for the current goal is (ap0_Sigma Empty (λ_ : set ⇒ V) (x,y) Hxy).
We prove the intermediate claim HxE: x ∈ Empty.
We will prove x ∈ Empty.
rewrite the current goal using (tuple_2_0_eq x y) (from right to left).
An exact proof term for the current goal is HxEmpty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
Let y be given.
Assume Hy: y ∈ Empty.
Apply (EmptyE y Hy) to the current goal.
∎