Let p be given.

Assume Hp: p ∈ f.

We will prove p ∈ graph X (λx : set ⇒ apply_fun f x).

We prove the intermediate claim HpXY: p ∈ setprod X Y.

An exact proof term for the current goal is (Hsub p Hp).

Apply (Sigma_E X (λ_ : set ⇒ Y) p HpXY) to the current goal.

Let x be given.

Assume Hxpair.

Apply Hxpair to the current goal.

Assume HxX Hexy.

Apply Hexy to the current goal.

Let y be given.

Assume Hypair.

Apply Hypair to the current goal.

Assume HyY HpEqPair.

We prove the intermediate claim HpEq: p = (x,y).

rewrite the current goal using HpEqPair (from left to right).

rewrite the current goal using (tuple_pair x y) (from left to right).

Use reflexivity.

We prove the intermediate claim Hxy: (x,y) ∈ f.

rewrite the current goal using HpEq (from right to left).

An exact proof term for the current goal is Hp.

We prove the intermediate claim Happ: apply_fun f x = y.

An exact proof term for the current goal is (functional_graph_apply_fun_eq f x y Hfun Hxy).

rewrite the current goal using HpEq (from left to right).

rewrite the current goal using Happ (from right to left).

An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ (x0,apply_fun f x0)) x HxX).

Let p be given.

Assume Hp: p ∈ graph X (λx : set ⇒ apply_fun f x).

We will prove p ∈ f.

Apply (ReplE_impred X (λx0 : set ⇒ (x0,apply_fun f x0)) p Hp (p ∈ f)) to the current goal.

Let x be given.

Assume HxX: x ∈ X.

Assume HpEq: p = (x,apply_fun f x).

rewrite the current goal using HpEq (from left to right).

We prove the intermediate claim Hex: ∃y : set, y ∈ Y ∧ (x,y) ∈ f.

An exact proof term for the current goal is (total_function_on_totality f X Y Htot x HxX).

We prove the intermediate claim Hex2: ∃y : set, (x,y) ∈ f.

Apply Hex to the current goal.

Let y be given.

Assume Hy: y ∈ Y ∧ (x,y) ∈ f.

We use y to witness the existential quantifier.

An exact proof term for the current goal is (andER (y ∈ Y) ((x,y) ∈ f) Hy).

An exact proof term for the current goal is (apply_fun_in_graph_of_ex f x Hex2).