Let X, Y and f be given.
Assume Hbij: bijection X Y f.
We will prove ∃h : set → set, bij X Y h.
We use (λx : set ⇒ apply_fun f x) to witness the existential quantifier.
Apply (bijI X Y (λx : set ⇒ apply_fun f x)) to the current goal.
Let u be given.
Assume HuX: u ∈ X.
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) (∀y : set, y ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x)) Hbij).
An exact proof term for the current goal is (Hfun u HuX).
Let u be given.
Assume HuX: u ∈ X.
Let v be given.
Assume HvX: v ∈ X.
Assume Heq: apply_fun f u = apply_fun f v.
Set y to be the term apply_fun f u.
We prove the intermediate claim Hydef: y = apply_fun f u.
Use reflexivity.
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 → ∃x : set, x ∈ X ∧ apply_fun f x = y0 ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x)) Hbij).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (Hfun u HuX).
We prove the intermediate claim HsurjU: ∀y0 : set, y0 ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y0 ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x).
An exact proof term for the current goal is (andER (function_on f X Y) (∀y0 : set, y0 ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y0 ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x)) Hbij).
We prove the intermediate claim Hex: ∃x0 : set, x0 ∈ X ∧ apply_fun f x0 = y ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x0).
An exact proof term for the current goal is (HsurjU y HyY).
Apply Hex to the current goal.
Let x0 be given.
Assume Hx0pack.
We prove the intermediate claim Huniq: ∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x0.
An exact proof term for the current goal is (andER (x0 ∈ X ∧ apply_fun f x0 = y) (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x0) Hx0pack).
We prove the intermediate claim Hu_y: apply_fun f u = y.
rewrite the current goal using Hydef (from left to right).
Use reflexivity.
We prove the intermediate claim Hv_y: apply_fun f v = y.
rewrite the current goal using Hydef (from left to right).
rewrite the current goal using Heq (from right to left).
Use reflexivity.
We prove the intermediate claim Hu0: u = x0.
An exact proof term for the current goal is (Huniq u HuX Hu_y).
We prove the intermediate claim Hv0: v = x0.
An exact proof term for the current goal is (Huniq v HvX Hv_y).
rewrite the current goal using Hu0 (from left to right).
rewrite the current goal using Hv0 (from right to left).
Use reflexivity.
Let w be given.
Assume HwY: w ∈ Y.
We prove the intermediate claim HsurjU: ∀y0 : set, y0 ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y0 ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x).
An exact proof term for the current goal is (andER (function_on f X Y) (∀y0 : set, y0 ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y0 ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y0 → x' = x)) Hbij).
We prove the intermediate claim Hex: ∃x0 : set, x0 ∈ X ∧ apply_fun f x0 = w ∧ (∀x' : set, x' ∈ X → apply_fun f x' = w → x' = x0).
An exact proof term for the current goal is (HsurjU w HwY).
Apply Hex to the current goal.
Let x0 be given.
Assume Hx0pack.
We use x0 to witness the existential quantifier.
We prove the intermediate claim Hx0pair: x0 ∈ X ∧ apply_fun f x0 = w.
An exact proof term for the current goal is (andEL (x0 ∈ X ∧ apply_fun f x0 = w) (∀x' : set, x' ∈ X → apply_fun f x' = w → x' = x0) Hx0pack).
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (x0 ∈ X) (apply_fun f x0 = w) Hx0pair).
An exact proof term for the current goal is (andER (x0 ∈ X) (apply_fun f x0 = w) Hx0pair).
∎