Let A, B, f and g be given.
Assume Hf Hg.
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply Hg to the current goal.
Assume Hg1 Hg2.
Set F to be the term
λX ⇒ {g y|y ∈ B ∖ {f x|x ∈ A ∖ X}} of type
set → set.
We prove the intermediate
claim L1:
∀U ∈ 𝒫 A, F U ∈ 𝒫 A.
Let U be given.
Assume HU.
We will
prove B ∖ {f x|x ∈ A ∖ U} ∈ 𝒫 B.
We prove the intermediate
claim L2:
∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V.
Let U be given.
Assume HU.
Let V be given.
Assume HV HUV.
We will
prove A ∖ V ⊆ A ∖ U.
An exact proof term for the current goal is HUV.
Let Y be given.
Assume H1.
Apply H1 to the current goal.
Set h to be the term
λx ⇒ if x ∈ Y then inv B g x else f x of type
set → set.
We will
prove ∃f : set → set, bij A B f.
We use h to witness the existential quantifier.
Apply bijI to the current goal.
Let x be given.
Assume Hx.
Apply xm (x ∈ Y) to the current goal.
rewrite the current goal using
If_i_1 (x ∈ Y) (inv B g x) (f x) H3 (from left to right).
We will
prove inv B g x ∈ B.
We prove the intermediate
claim L1:
x ∈ F Y.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H3.
Let y be given.
We prove the intermediate
claim L2:
y ∈ B.
An
exact proof term for the current goal is
setminusE1 B {f x|x ∈ A ∖ Y} y H4.
rewrite the current goal using H5 (from left to right).
We will
prove inv B g (g y) ∈ B.
rewrite the current goal using
inj_linv B g Hg2 y L2 (from left to right).
An exact proof term for the current goal is L2.
rewrite the current goal using
If_i_0 (x ∈ Y) (inv B g x) (f x) H3 (from left to right).
Apply Hf1 to the current goal.
An exact proof term for the current goal is Hx.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply xm (x ∈ Y) to the current goal.
rewrite the current goal using
If_i_1 (x ∈ Y) (inv B g x) (f x) H3 (from left to right).
We prove the intermediate
claim Lx:
x ∈ F Y.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H3.
Let z be given.
Assume Hz1a Hz1b.
Apply xm (y ∈ Y) to the current goal.
rewrite the current goal using
If_i_1 (y ∈ Y) (inv B g y) (f y) H4 (from left to right).
We will
prove inv B g x = inv B g y → x = y.
We prove the intermediate
claim Ly:
y ∈ F Y.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H4.
Let w be given.
rewrite the current goal using Hz2 (from left to right).
rewrite the current goal using Hw2 (from left to right).
rewrite the current goal using
inj_linv B g Hg2 z Hz1a (from left to right).
Use f_equal.
An exact proof term for the current goal is H5.
rewrite the current goal using
If_i_0 (y ∈ Y) (inv B g y) (f y) H4 (from left to right).
We will
prove inv B g x = f y → x = y.
rewrite the current goal using Hz2 (from left to right).
rewrite the current goal using
inj_linv B g Hg2 z Hz1a (from left to right).
We will
prove z = f y → g z = y.
Apply Hz1b to the current goal.
We will
prove z ∈ {f x|x ∈ A ∖ Y}.
rewrite the current goal using H5 (from left to right).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is H4.
rewrite the current goal using
If_i_0 (x ∈ Y) (inv B g x) (f x) H3 (from left to right).
Apply xm (y ∈ Y) to the current goal.
rewrite the current goal using
If_i_1 (y ∈ Y) (inv B g y) (f y) H4 (from left to right).
We will
prove f x = inv B g y → x = y.
We prove the intermediate
claim Ly:
y ∈ F Y.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H4.
Let w be given.
Assume Hw1a Hw1b.
rewrite the current goal using Hw2 (from left to right).
rewrite the current goal using
inj_linv B g Hg2 w Hw1a (from left to right).
Apply Hw1b to the current goal.
We will
prove w ∈ {f x|x ∈ A ∖ Y}.
rewrite the current goal using H5 (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is H3.
rewrite the current goal using
If_i_0 (y ∈ Y) (inv B g y) (f y) H4 (from left to right).
We will
prove f x = f y → x = y.
An exact proof term for the current goal is Hf2 x Hx y Hy.
Let w be given.
Apply xm (w ∈ {f x|x ∈ A ∖ Y}) to the current goal.
Let x be given.
Apply setminusE A Y x H4 to the current goal.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H6.
rewrite the current goal using
If_i_0 (x ∈ Y) (inv B g x) (f x) H7 (from left to right).
Use symmetry.
An exact proof term for the current goal is H5.
We prove the intermediate
claim Lgw:
g w ∈ Y.
rewrite the current goal using H2 (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hw.
We will
prove w ∉ {f x|x ∈ A ∖ Y}.
An exact proof term for the current goal is H3.
We use (g w) to witness the existential quantifier.
Apply andI to the current goal.
Apply Hg1 to the current goal.
An exact proof term for the current goal is Hw.
rewrite the current goal using
If_i_1 (g w ∈ Y) (inv B g (g w)) (f (g w)) Lgw (from left to right).
An
exact proof term for the current goal is
inj_linv B g Hg2 w Hw.
∎