Let X, Y, Z, f and g be given.
Assume Hf: bijection X Y f.
Assume Hg: bijection Y Z g.
We prove the intermediate claim Hf_fun: function_on f X Y.
An exact proof term for the current goal is (andEL (function_on f X Y) (∀y : set, y ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x)) Hf).
We prove the intermediate claim Hg_fun: function_on g Y Z.
An exact proof term for the current goal is (andEL (function_on g Y Z) (∀z : set, z ∈ Z → ∃y : set, y ∈ Y ∧ apply_fun g y = z ∧ (∀y' : set, y' ∈ Y → apply_fun g y' = z → y' = y)) Hg).
We prove the intermediate claim Hf_surjU: ∀y : set, y ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x).
An exact proof term for the current goal is (andER (function_on f X Y) (∀y : set, y ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x)) Hf).
We prove the intermediate claim Hg_surjU: ∀z : set, z ∈ Z → ∃y : set, y ∈ Y ∧ apply_fun g y = z ∧ (∀y' : set, y' ∈ Y → apply_fun g y' = z → y' = y).
An exact proof term for the current goal is (andER (function_on g Y Z) (∀z : set, z ∈ Z → ∃y : set, y ∈ Y ∧ apply_fun g y = z ∧ (∀y' : set, y' ∈ Y → apply_fun g y' = z → y' = y)) Hg).
We will prove function_on (compose_fun X f g) X Z ∧ (∀z : set, z ∈ Z → ∃x : set, x ∈ X ∧ apply_fun (compose_fun X f g) x = z ∧ (∀x' : set, x' ∈ X → apply_fun (compose_fun X f g) x' = z → x' = x)).
Apply andI to the current goal.
An exact proof term for the current goal is (function_on_compose_fun X Y Z f g Hf_fun Hg_fun).
Let z be given.
Assume HzZ: z ∈ Z.
We prove the intermediate claim Hexy: ∃y0 : set, y0 ∈ Y ∧ apply_fun g y0 = z ∧ (∀y' : set, y' ∈ Y → apply_fun g y' = z → y' = y0).
An exact proof term for the current goal is (Hg_surjU z HzZ).
Apply Hexy to the current goal.
Let y0 be given.
Assume Hy0pack.
We prove the intermediate claim Hy0pair: y0 ∈ Y ∧ apply_fun g y0 = z.
An exact proof term for the current goal is (andEL (y0 ∈ Y ∧ apply_fun g y0 = z) (∀y' : set, y' ∈ Y → apply_fun g y' = z → y' = y0) Hy0pack).
We prove the intermediate claim Hy0Y: y0 ∈ Y.
An exact proof term for the current goal is (andEL (y0 ∈ Y) (apply_fun g y0 = z) Hy0pair).
We prove the intermediate claim Hy0eq: apply_fun g y0 = z.
An exact proof term for the current goal is (andER (y0 ∈ Y) (apply_fun g y0 = z) Hy0pair).
We prove the intermediate claim Hyuniq: ∀y' : set, y' ∈ Y → apply_fun g y' = z → y' = y0.
An exact proof term for the current goal is (andER (y0 ∈ Y ∧ apply_fun g y0 = z) (∀y' : set, y' ∈ Y → apply_fun g y' = z → y' = y0) Hy0pack).
We prove the intermediate claim Hexx: ∃x0 : set, x0 ∈ X ∧ apply_fun f x0 = y0 ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x0).
An exact proof term for the current goal is (Hf_surjU y0 Hy0Y).
Apply Hexx to the current goal.
Let x0 be given.
Assume Hx0pack.
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim Hx0pair: x0 ∈ X ∧ apply_fun f x0 = y0.
An exact proof term for the current goal is (andEL (x0 ∈ X ∧ apply_fun f x0 = y0) (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x0) Hx0pack).
An exact proof term for the current goal is (andEL (x0 ∈ X) (apply_fun f x0 = y0) Hx0pair).
We prove the intermediate claim Hx0pair: x0 ∈ X ∧ apply_fun f x0 = y0.
An exact proof term for the current goal is (andEL (x0 ∈ X ∧ apply_fun f x0 = y0) (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x0) Hx0pack).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (andEL (x0 ∈ X) (apply_fun f x0 = y0) Hx0pair).
We prove the intermediate claim Hfx0: apply_fun f x0 = y0.
An exact proof term for the current goal is (andER (x0 ∈ X) (apply_fun f x0 = y0) Hx0pair).
rewrite the current goal using (compose_fun_apply X f g x0 Hx0X) (from left to right).
rewrite the current goal using Hfx0 (from left to right).
An exact proof term for the current goal is Hy0eq.
Let x' be given.
Assume Hx'X: x' ∈ X.
Assume Hx'Eq: apply_fun (compose_fun X f g) x' = z.
We prove the intermediate claim Hxuniq: ∀x1 : set, x1 ∈ X → apply_fun f x1 = y0 → x1 = x0.
An exact proof term for the current goal is (andER (x0 ∈ X ∧ apply_fun f x0 = y0) (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x0) Hx0pack).
We prove the intermediate claim Hy': apply_fun f x' ∈ Y.
An exact proof term for the current goal is (Hf_fun x' Hx'X).
We prove the intermediate claim Hgy': apply_fun g (apply_fun f x') = z.
rewrite the current goal using (compose_fun_apply X f g x' Hx'X) (from right to left).
An exact proof term for the current goal is Hx'Eq.
We prove the intermediate claim HyEq: apply_fun f x' = y0.
An exact proof term for the current goal is (Hyuniq (apply_fun f x') Hy' Hgy').
An exact proof term for the current goal is (Hxuniq x' Hx'X HyEq).
∎