Suppose we have sets x and y, and injections f: x -> y and g: y -> x
Set(x) (x is a set) & Set(y) (y is a set) & ALL(a):[a e x => f(a) e y] (f: x -> y) & ALL(a):[a e y => g(a) e x] (g: y -> x) & Injection(f,x,y) (f is an injection) & Injection(g,y,x) (g is an injection)
then there exists bijection k: x -> y
ALL(a):[a e x => k(a) e y] (k: x -> y) & Bijection(k,x,y) (k is a bijection)
where e = epsilon (set membership)
We start with sets x and y, injections f: x -> y and g: y -> x
From these, we construct, using the axioms of set theory and previously established lemmas, various sets and functions that will be required:
px = the power set of x py = the power set of y px2 = the Cartesian prouduct of px with itself xy = the Cartesian prouduct of x and y imgF(s) = the image of s under f imgG(s) = the image of s under g cx(s) = the complement of s relative to x cy(s) = the complement of s relative to y h(s) = cx(imgG(cy(imgF(s)))) g' = the inverse of a suitable restriction (subset) of g
Then we prove that for subsets s1 and s1 of x, if s1 is a subset of s2, then h(s1) is also a subset of h(s2). We say that h is increasing.
Using the Knaster-Tarski Fixed-Point Lemma, we establish the existence of a subset z of x such h(z)=z.
Then we construct the function k: x -> y such that