Let X, Y, f and A be given.
Assume Hbij: bijection X Y f.
Assume HA: A ⊆ X.
Set g to be the term inv_fun_graph X f Y.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ preimage_of Y g A.
We will prove y ∈ image_of_fun f A.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λu : set ⇒ apply_fun g u ∈ A) y Hy).
We prove the intermediate claim HgyA: apply_fun g y ∈ A.
An exact proof term for the current goal is (SepE2 Y (λu : set ⇒ apply_fun g u ∈ A) y Hy).
We prove the intermediate claim Heq: apply_fun f (apply_fun g y) = y.
An exact proof term for the current goal is (inv_fun_graph_right_inverse X Y f y Hbij HyY).
We prove the intermediate claim HyImg: apply_fun f (apply_fun g y) ∈ image_of_fun f A.
An exact proof term for the current goal is (ReplI A (λx0 : set ⇒ apply_fun f x0) (apply_fun g y) HgyA).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyImg.
Let y be given.
Assume Hy: y ∈ image_of_fun f A.
We will prove y ∈ preimage_of Y g A.
Apply (ReplE_impred A (λx0 : set ⇒ apply_fun f x0) y Hy) to the current goal.
Let x be given.
Assume HxA: x ∈ A.
Assume Heq: y = apply_fun f x.
We will prove y ∈ {u ∈ Y|apply_fun g u ∈ A}.
Apply SepI to the current goal.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim Hfun: function_on f X Y.
An exact proof term for the current goal is (andEL (function_on f X Y) (∀y0 : set, y0 ∈ Y → ∃x0 : set, x0 ∈ X ∧ apply_fun f x0 = y0 ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x0)) Hbij).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Hfun x HxX).
We will prove apply_fun g y ∈ A.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim Hinv: apply_fun g (apply_fun f x) = x.
An exact proof term for the current goal is (inv_fun_graph_left_inverse X Y f x Hbij HxX).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is HxA.
∎