Thm*  InvFuns(A;B;f;g)  Bij(A; B; f)

First note the key definitions:

Def  InvFuns(A;B;f;g) == (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)

Def  Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)

It turns out that each conjunct of the conclusion will follow from a conjunct of the premise, namely,

(x:A. g(f(x)) = x)  Inj(A; B; f), and

(y:B. f(g(y)) = y)  Surj(A; B; f).

To show Inj(A; B; f) is just to show that

f(a1) = f(a2)  a1 = a2, which is so since

f(a1) = f(a2)  g(f(a1)) = g(f(a2)), and g cancels f by assumption,

so, a1 = a2.

To show Surj(A; B; f) is just to show that

b:B. a:A. f(a) = b

which is witnessed by g(b) thus:

b:B. f(g(b)) = b, which follows from our assumption.

QED

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html