Nuprl - Proof: one one corr rel vs invfuns 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr rel vs invfuns 1 1 1

1. A : Type
2. B : Type
3. R : A

Prop
4.

x:A.

!y:B. R(x;y)
5.

y:B.

!x:A. R(x;y)

f:(A

B), g:(B

A).

InvFuns(A;B;f;g) & (

x:A, y:B. R(x;y)

y = f(x) & x = g(y))

By:	FwdThru: Thm* (x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x))) on [ Hyp:4 ] THEN SimilarTo: Hyp:-1 THEN FwdThru: Thm* (x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x))) on [ Hyp:5 ] THEN CBV-1: g THEN SimilarTo: Hyp:-1

Generated subgoal:

1 6. f : AB
7. x:A. R(x;f(x))
8. g : BA
9. y:B. R(g(y);y)
InvFuns(A;B;f;g) & (x:A, y:B. R(x;y) y = f(x) & x = g(y))
22 steps

About:

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