Let X, Y, f and y be given.
Assume Hy: y ∈ Y.
We will prove apply_fun (inv_fun_graph X f Y) y = inv X (λx : set ⇒ apply_fun f x) y.
We will prove apply_fun {(y0,inv X (λx : set ⇒ apply_fun f x) y0)|y0 ∈ Y} y = inv X (λx : set ⇒ apply_fun f x) y.
We will prove Eps_i (λz ⇒ (y,z) ∈ {(y0,inv X (λx : set ⇒ apply_fun f x) y0)|y0 ∈ Y}) = inv X (λx : set ⇒ apply_fun f x) y.
We prove the intermediate claim H1: (y,inv X (λx : set ⇒ apply_fun f x) y) ∈ {(y0,inv X (λx : set ⇒ apply_fun f x) y0)|y0 ∈ Y}.
An exact proof term for the current goal is (ReplI Y (λy0 : set ⇒ (y0,inv X (λx : set ⇒ apply_fun f x) y0)) y Hy).
We prove the intermediate claim H2: (y,Eps_i (λz ⇒ (y,z) ∈ {(y0,inv X (λx : set ⇒ apply_fun f x) y0)|y0 ∈ Y})) ∈ {(y0,inv X (λx : set ⇒ apply_fun f x) y0)|y0 ∈ Y}.
An exact proof term for the current goal is (Eps_i_ax (λz ⇒ (y,z) ∈ {(y0,inv X (λx : set ⇒ apply_fun f x) y0)|y0 ∈ Y}) (inv X (λx : set ⇒ apply_fun f x) y) H1).
Apply (ReplE_impred Y (λy0 : set ⇒ (y0,inv X (λx : set ⇒ apply_fun f x) y0)) (y,Eps_i (λz ⇒ (y,z) ∈ {(y0,inv X (λx : set ⇒ apply_fun f x) y0)|y0 ∈ Y})) H2) to the current goal.
Let y0 be given.
Assume Hy0: y0 ∈ Y.
Assume Heq: (y,Eps_i (λz ⇒ (y,z) ∈ {(y1,inv X (λx : set ⇒ apply_fun f x) y1)|y1 ∈ Y})) = (y0,inv X (λx : set ⇒ apply_fun f x) y0).
We prove the intermediate claim Hy_eq: y = y0.
rewrite the current goal using (tuple_2_0_eq y (Eps_i (λz ⇒ (y,z) ∈ {(y1,inv X (λx : set ⇒ apply_fun f x) y1)|y1 ∈ Y}))) (from right to left).
rewrite the current goal using (tuple_2_0_eq y0 (inv X (λx : set ⇒ apply_fun f x) y0)) (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 ⇒ (y,z) ∈ {(y1,inv X (λx : set ⇒ apply_fun f x) y1)|y1 ∈ Y}) = inv X (λx : set ⇒ apply_fun f x) y0.
rewrite the current goal using (tuple_2_1_eq y (Eps_i (λz ⇒ (y,z) ∈ {(y1,inv X (λx : set ⇒ apply_fun f x) y1)|y1 ∈ Y}))) (from right to left).
rewrite the current goal using (tuple_2_1_eq y0 (inv X (λx : set ⇒ apply_fun f x) y0)) (from right to left).
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 Hy_eq (from right to left).
Use reflexivity.
∎